Paper Info
Title
Partial, total and general correctness
Abstract
We identify weak semirings, which drop the right annihilation axiom a0 = 0, as a common foundation for partial, total and general correctness. It is known how to extend weak semirings by operations for finite and infinite iteration and domain. We use the resulting weak omega algebras with domain to define a semantics of while-programs which is valid in all three correctness approaches. The unified, algebraic semantics yields program transformations at once for partial, total and general correctness. We thus give a proof of the normal form theorem for while-programs, which is a new result for general correctness and extends to programs with non-deterministic choice. By adding specific axioms to the common ones, we obtain partial, total or general correctness as a specialisation. We continue our previous investigation of axioms for general correctness. In particular, we show that a subset of these axioms is sufficient to derive a useful theory, which includes the Egli-Milner order, full recursion, correctness statements and a correctness calculus. We also show that this subset is necessary.
Year
DOI
Venue
2010
10.1007/978-3-642-13321-3_11
MPC
Keywords
Field
DocType
correctness statement,common foundation,full recursion,egli-milner order,weak semirings,general correctness,algebraic semantics yields program,weak omega algebra,correctness calculus,correctness approach,normal form
Discrete mathematics,Program transformation,Axiom,Correctness,Hoare logic,Semantics,Recursion,Mathematics,Algebraic semantics
Conference
Volume
ISSN
ISBN
6120
0302-9743
3-642-13320-7
Citations 
PageRank 
References 
10
0.49
28
Authors
1
Name
Order
Citations
PageRank
Walter Guttmann119616.53