2013/05/24 by Emil Sekerinski, Tian Zhang
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Software Testing and Debugging Techniques #cs.LO
paper · pdf · doi:10.4204/eptcs.115.1
published as EPTCS 115, 2013, pp. 1-14 · In Proceedings Refine 2013, arXiv:1305.5634
openalex publication_date 2013/05/24 · arxiv created 2013/05/27 · arxiv updated 2013/05/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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.