zbMATH — the first resource for mathematics

A weakest precondition semantics for an object-oriented language of refinement. (English) Zbl 0953.68081
Wing, Jeannette M. (ed.) et al., FM ’99. Formal methods. World congress on Formal methods in the development of computing systems. Toulouse, France, September 20–24, 1999. Proceedings. In 2 vols. Berlin: Springer (ISBN 3-540-66587-0/vol1; 3-540-66588-9/vol2). Lect. Notes Comput. Sci. 1708; 1709, 1439-1459 (1999).
Summary: We define a predicate-transformer semantics for an object-oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility control, dynamic binding, and recursive methods. Using the semantics, we formulate notions of refinement. Such results are a first step towards a refinement calculus.
For the entire collection see [Zbl 0929.00076].

68Q55 Semantics in the theory of computing