| Autor: |
Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, Aagaard, Mark, Harrison, John, Laibinis, Linas, von Wright, Joakim |
| Zdroj: |
Theorem Proving in Higher Order Logics (9783540678632); 2000, p372-387, 16p |
| Abstrakt: |
In this paper we present an approach for modelling functional procedures (as they occur in imperative programming languages) in a weakest precondition framework. Functional procedures are called inside expressions, but the body of a functional procedure is built using standard specification/programming syntax, including nondeterminism, sequential composition, conditionals and loops. We integrate our theory of functional procedures into the existing mechanisation of the refinement calculus in the HOL system. To make formal reasoning possible, we derive correctness rules for functional procedures and their calls. We also show how recursive functional procedures can be handled according to our approach. Finally, we provide a nontrivial example of reasoning about a recursive procedure for binary search. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
