Hoare's logic and VDM

Hoare's logic and VDM
http://www.springerlink.com/content/mk583100700h6ux0/

by J. Coenen1 Contact

Received: 15 August 1993 Accepted: 15 March 1994

Abstract

A relational framework which unifies Hoare's logic and VDM is presented. Within this framework a partial correctness version of VDM is defined. It is argued that this partial correctness version of VDM is intuitive and consistent with the original total correctness version. Furthermore it is shown how both partial and total correctness formulae and specifications can be translated from Hoare's logic into VDM and vice versa. VDM's satisfiability requirement is briefly discussed, and a similar condition for Hoare's logic is defined.:

Keywords Hoare's logic - Program specification - Realizability - VDM
Supported by NWO/SION project 612-316-103: lsquoFault Tolerance: Paradigms, Models, Logics, Construction.rsquo