Operational semantics and generalized weakest preconditions

DOI10.1016/0167-6423(94)90010-8MaRDI QIDQ1330453zbMATH OpenOpenAlexFDO

Authors Johan L. Lukkien

Publication date 21 July 1994

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(94)90010-8

zbMATH Keywords

operational semanticstemporal propertyunfoldingweakest precondition

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Review text

Part of this paper was part of author's thesis (1991). It presents an operational semantics for the guarded command languages in which a computation is defined explicitly as a sequence of states through which execution of the program may evolve, starting from a certain initial state. The main contribution is a generalization of the Dijkstra's notion of weakest precondition. This generalization supports reasoning about general properties of programs, including temporal properties. Also, definition of the repetition was given in a closed form, which allowed the author to derive that repetition is equivalent to its first unfolding. Repetition has been defined both as the solution of a recursive equation and as the limit of its unfoldings. The author presents how to introduce the temporal property ``ever and the property ``leads-to. By the so-called action systems a new theorem is proved.

Recommendations

• Formal Methods in Computer-Aided Design
• Structural operational semantics for weak bisimulations
• A proof theoretic approach to operational semantics
• scientific article; zbMATH DE number 65532
• scientific article; zbMATH DE number 1424026
• Formal foundations of operational semantics
• Inductive assertions and operational semantics
• Operational semantics with semicommutations
• Structural operational semantics and bounded nondeterminism

Cited in

(7)

• The weakest precondition calculus: Recursion and duality
• Safety and progress of recursive procedures
• Weakest relative precondition semantics. Balancing approved theory and realistic translation verification
• Guards, failure, and partiality: Dijkstra's guarded-command language formulated topologically
• Formal semantics for program paths
• scientific article; zbMATH DE number 794263 (Why is no real title available?)
• Structural operational semantics for weak bisimulations

This page was built for publication: Operational semantics and generalized weakest preconditions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1330453)