Share This Article:

A Logical Treatment of Non-Termination and Program Behaviour

Abstract Full-Text HTML Download Download as PDF (Size:295KB) PP. 555-561
DOI: 10.4236/jsea.2014.77051    3,972 Downloads   4,556 Views  


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.

Cite this paper

Ward, M. and Zedan, H. (2014) A Logical Treatment of Non-Termination and Program Behaviour. Journal of Software Engineering and Applications, 7, 555-561. doi: 10.4236/jsea.2014.77051.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] Ward, M. (2004) Pigs from Sausages? Reengineering from Assembler to C via Fermat Transformations. Science of Computer Programming, Special Issue on Program Transformation, 52, 213-255.
[2] Dijkstra, E.W. (1976) A Discipline of Programming. Prentice-Hall, Englewood Cli?s.
[3] Moszkowski, B. (1994) Some Very Compositional Temporal Properties. In: Olderog, E.-R., Ed., Programming Concepts, Methods and Calculi, IFIP Transactions, North-Holland Publishing Co., Amsterdam, 307-326.

comments powered by Disqus

Copyright © 2020 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.