A unified approach of program verification.

*(English)*Zbl 1414.68019Summary: The subject of this paper is a program verification method that takes into account abortion caused by partial functions in program statements. In particular, boolean expressions of various statements will be investigated that are not well-defined. For example, a loop aborts if its execution begins in a state for which the loop condition is undefined. This work considers the program constructs of nondeterministic sequential programs and also deals with the synchronization statement of parallel programs introduced by S. Owicki and D. Gries [Acta Inf. 6, 319–340 (1976; Zbl 0312.68011)]. The syntax of program constructs will be reviewed and their semantics will be formally defined in such a way that they suit the relational model of programming developed at Eötvös Loránd University [Á. Fóthi, Ann. Univ. Sci. Budap. Rolando Eötvös, Sect. Comput. 9, 105–113 (1988; Zbl 0723.68023); Á. Fóthi et al., “Some concepts of a relation model of programming”, in: Proceedings of the 4th symposium on programming language and software tools, SPLST’95. 434–446 (1995)]. This relational model defines the program as a set of its possible executions and also provides definition for other important programming notions like problem and solution. The proof rules of total correctness will be extended by treating abortion caused by partial functions. The use of these rules will be demonstrated by means of a verification case study.

##### MSC:

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

68Q60 | Specification and verification (program logics, model checking, etc.) |

PDF
BibTeX
XML
Cite

\textit{T. Gregorics} and \textit{Z. Borsi}, Acta Univ. Sapientiae, Inform. 9, No. 1, 65--82 (2017; Zbl 1414.68019)

Full Text:
DOI

**OpenURL**

##### References:

[1] | K. R. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Program, Springer-Verlag, 1997. )67 · Zbl 0869.68064 |

[2] | E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, Englewood Clifis, New York, 1976. )65, 68, 73 · Zbl 0368.68005 |

[3] | Á. Fóthi, Mathematical Approach to Programming, Ann. Univ. Sci. Budapest. Sect. Comput. 9 (1988) 105-114. )65, 68 |

[4] | Á. Fóthi et al, Some concepts of a Relational Model of Programming, Proc. 4th Symposium on Programming Language and Software Tools, Visegrfiad, Hungary, June 8-14, 1995. (ed. Varga L.,) pp. 434-446, )65 |

[5] | Á. Fóthi, Bevezetfies a programozfiashoz, ELTE Eőtvős Kiadó. 2005. (in Hungarian). )65, 68 |

[6] | T. Gregorics, Concept of abstract program, Acta Universitatis Sapientiae, In- formatica, 4, 1 (2012) 7-16. )68, 69 · Zbl 1317.68032 |

[7] | D. Gries, S. Owicki, An axiomatic proof technique for parallel programs, Acta Inf., 6, 4 (1976) 319-340. )65, 73 · Zbl 0312.68011 |

[8] | D. Gries, The Science of Programming, Springer, Berlin, 1981. )65, 67, 73 · Zbl 0472.68003 |

[9] | C. A. Hoare, An axiomatic basis for computer programming, Comm. of the ACM 12, 10 (1969) 576-580. )65, 67, 73 · Zbl 0179.23105 |

[10] | Z. Manna, Mathematical theory of computation, McGraw Hill, 1974. )67 · Zbl 0353.68066 |

[11] | W.-P. de Roever et al, Concurrency Verification, Cambridge University Press, 2001. )67 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.