Query:
faculty: "FNWI" and publication year: "1997"
| Author | Marc Pauly | | Title | Transforming Predicates or Updating States? Total Correctness in Dynamic Logic and Structured Programming |
| Year | 1997 |
| Faculty | Faculty of Science |
| Institute/dept. | FNWI/FGw: Institute for Logic, Language and Computation (ILLC) |
| Series | ILLC Master of Logic Theses / ILLC ; MoL-1997-03 |
| Abstract | Transforming Predicates or Updating States?
Total Correctness in Dynamic Logic and Structured Programming
Marc Pauly
On a very general level, the goal of this paper is a comparison between two
semantic traditions, the predicate transformer tradition in the style of
Dijkstra and the more standard state transformer tradition in the style of
e.g. Dynamic Logic. Since state�transformer (ST ) semantics seem to be much
more well�known and more frequently applied than predicate�transformer (PT )
semantics, this paper will concentrate on the PT �approach and connecting it
to the ST �approach rather than vice versa. Hence, part of this paper can also
serve as an introduction to PT�semantics for ST�semanticists, especially
sections 2 and 3.
The two traditions will be compared on three increasingly concrete levels:
(1) on the abstract set�theoretic level where predicate transformers and state
transformers are viewed as abstract functions, (2) on the level of the classes
of transformers which are associated with particular programming languages,
such as the WHILE language or the guarded�command language, (3) on the level of
logical implementation, i.e. by investigating logics in which we can formalize
(for a given class of programs) predicate transformers on the one hand and
state transformers on the other hand. While most of the general results used in
this comparison are not new, we think that the comparison has not yet been done
in such a systematic fashion, especially regarding the three program classes
just mentioned. Furthermore, as a result of this comparison we propose a new
logic called PDL^pt which is a propositional dynamic logic with PT�semantics.
It will be argued that this logic is a rather general framework for reasoning
about the total correctness of programs and actions more generally. |
| Document type | Preprint |
| Download paper | |
| Document finder | 
|
Use this url to link to this page: http://dare.uva.nl/en/record/419849
Contact us about this recordNotify a colleague
Add to bookbag
|
previous 1866 next 
