Operational semantics and generalized weakest preconditions
type: Item
instance of: scholarly article
title: Operational semantics and generalized weakest preconditions
zbMATH Open document ID: 0814.68086
DOI: 10.1016/0167-6423(94)90010-8
author: Johan L. Lukkien
published in: Science of Computer Programming
publication date: 1994-07-21T00:00:00Z
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.
reviewed by: Doina Tatar
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 609582
zbMATH Keywords: operational semantics
zbMATH Keywords: weakest precondition
zbMATH Keywords: unfolding
zbMATH Keywords: temporal property
MaRDI profile type: Publication
full work available at URL: 0167-6423(94)90010-8
OpenAlex ID: W2074792671
Recommended article: Formal Methods in Computer-Aided Design
Recommended article: Structural operational semantics for weak bisimulations
Recommended article: A Proof Theoretic Approach to Operational Semantics
Recommended article: Q4012880
Recommended article: Q4945216
Recommended article: Formal foundations of operational semantics
Recommended article: Correct Hardware Design and Verification Methods
Recommended article: Operational semantics with semicommutations
Recommended article: Structural operational semantics and bounded nondeterminism
description: scientific article; zbMATH DE number 609582