A Logical Treatment of Non-Termination and Program BehaviourReportar como inadecuado




A Logical Treatment of Non-Termination and Program Behaviour - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Can the semantics of aprogram be represented as a single formula? We show that one formula isinsufficient to handle assertions, refinement or slicing, while two formulaeare sufficient: A S , definingnon-termination, and B S, definingbehaviour. Any two formulae B will define a correspondingprogram. Refinement is defined as implication between these formulae.

KEYWORDS

Formal Methods, Refinement, Non-Termination, Non-Determinism, Weakest Precondition, Temporal Logic, Wide-Spectrum Language

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.





Autor: Martin Ward, Hussein Zedan

Fuente: http://www.scirp.org/



DESCARGAR PDF




Documentos relacionados