Thumbnail
Access Restriction
Subscribed

Author Shankar, A. Udaya
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1993
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Hoare logic ♦ Assertional reasoning ♦ Generation of preconditions ♦ Invariants ♦ Leads-to ♦ Progress properties ♦ Safety properties ♦ State transition systems ♦ Weakest preconditions
Abstract This is a tutorial introduction to assertional reasoning based on temporal logic. The objective is to provide a working familiarity with the technique. We use a simple system model and a simple proof system, and we keep to a minimum the treatment of issues such as soundness, completeness, compositionality, and abstraction. We model a concurrent system by a state transition system and fairness requirements. We reason about such systems using Hoare logic and a subset of linear-time temporal logic, specifically, invariant assertions and leads-to assertions. We apply the method to several examples.
ISSN 03600300
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1993-09-01
Publisher Place New York
e-ISSN 15577341
Journal ACM Computing Surveys (CSUR)
Volume Number 25
Issue Number 3
Page Count 38
Starting Page 225
Ending Page 262


Open content in new tab

   Open content in new tab
Source: ACM Digital Library