TITLE:
A Logical Treatment of Non-Termination and Program Behaviour
AUTHORS:
Martin Ward, Hussein Zedan
KEYWORDS:
Formal Methods, Refinement, Non-Termination, Non-Determinism, Weakest Precondition, Temporal Logic, Wide-Spectrum Language
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.7 No.7,
June
5,
2014
ABSTRACT: Can the semantics of a
program be represented as a single formula? We show that one formula is
insufficient to handle assertions, refinement or slicing, while two formulae
are sufficient: A (S) , defining
non-termination, and B (S), defining
behaviour. Any two formulae A and B will define a corresponding
program. Refinement is defined as implication between these formulae.