Journal of Software Engineering and Applications
Volume 7, Issue 7 (June 2014)
ISSN Print: 1945-3116 ISSN Online: 1945-3124
Google-based Impact Factor: 1.22 Citations h5-index & Ranking
A Logical Treatment of Non-Termination and Program Behaviour ()
Affiliation(s)
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.
KEYWORDS
Share and Cite:
Cited by
Copyright © 2024 by authors and Scientific Research Publishing Inc.
This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.