Research ArticleOpen AccessGoogle Scholar indexed
A Logical Treatment of Non-Termination and Program Behaviour
Software Technology Research Lab, De Montfort University, Leicester, UK
Applied Science University, Al Eker, Bahrain
- 1 Software Technology Research Lab, De Montfort University, Leicester, UK
- 2 Applied Science University, Al Eker, Bahrain
Journal of Software Engineering and Applications·Volume 07 (2014)·Pages 555–561·Published 5 June 2014·DOI10.4236/jsea.2014.77051
Copy link · social · email
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.
KeywordsFormal MethodsRefinementNon-TerminationNon-DeterminismWeakest PreconditionTemporal LogicWide-Spectrum Language
- 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. http://www.gkc.org.uk/martin/papers/migration-t.pdf
- Dijkstra, E.W. (1976) A Discipline of Programming. Prentice-Hall, Englewood Cli?s.
- 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.