On a New Notion of Partial Refinement

TL;DR

This paper introduces a novel concept of partial refinement in program development, enabling implementations to terminate exceptionally when necessary, thus facilitating systematic exception handling in software refinement.

Contribution

It proposes a new notion of partial refinement that allows partial implementations with exceptional termination, advancing formal methods for practical program development.

Findings

Defines a new partial refinement concept for programs with exceptions

Provides a systematic method for developing exception-handling programs

Enhances formal specification techniques with practical partial implementations

Abstract

Formal specification techniques allow expressing idealized specifications, which abstract from restrictions that may arise in implementations. However, partial implementations are universal in software development due to practical limitations. Our goal is to contribute to a method of program refinement that allows for partial implementations. For programs with a normal and an exceptional exit, we propose a new notion of partial refinement which allows an implementation to terminate exceptionally if the desired results cannot be achieved, provided the initial state is maintained. Partial refinement leads to a systematic method of developing programs with exception handling.