Tool Support for Invariant Based Programming

14 years 29 days ago
Tool Support for Invariant Based Programming
— Invariant based programming is an approach to program construction where we provide the program pre- and postconditions as well as loop invariants before we construct the code itself. This approach allows us to construct a program and its correctness proof hand in hand. We describe here an extension to an existing mathematics editor that supports this style of program construction. The main help that the tool provides is automatic simplification of verification conditions that are generated in the programming process. The tool shows the user a check list of those conditions that it was not able to prove automatically. The user can use this check list to complete the proof (either manually or using an interactive theorem prover) or to find errors in the program.
Ralph-Johan Back, Magnus Myreen
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Authors Ralph-Johan Back, Magnus Myreen
Comments (0)