作者: Andrii Kryvolap , Mykola Nikitchenko , Wolfgang Schreiner
DOI: 10.1007/978-3-319-03998-5_18
关键词:
摘要: Traditional (classical) Floyd-Hoare logic is defined for a case of total pre- and postconditions while programs can be partial. In the chapter we propose to extend this partial conditions. To do first construct investigate special program algebras predicates, functions, programs. such correctness assertions are presented with help composition called composition. This monotone continuous. Considering class constructed as semantic base then define an extended – Partial Logic its properties. has rather complicated soundness constraints inference rules, therefore simpler sufficient proposed. The used verification.