00000cab a22000003a 4500 UP-99796217608834987 Buklod 20231007234841.0 m |o d | ta 090512s xx d | ||r ||||| || DENGII eng Barnett, Mike Weakest-precondition of unstructured programs. pp. 24 Program verification systems typically transform a program into a logical expression which is then fed to a theorem prover. The logical expression represents the weakest precondition of the program relative to its specification; when (and if!) the theorem prover is able to prove the expression, then the program is considered correct. Computing such a logical expression for an imperative, structured program is straightforward, although there are issues having to do with loops and the efficiency both of the computation and of the complexity of the formula with respect to the theorem prover. This paper presents a novel approach for computing the weakest precondition of an unstructured program that is sound even in the presence of loops. The computation is efficient and the resulting logical expression provides more leeway for the theorem prover efficiently to attack the proof. Software. Software engineering. Software / Program Verification. Coding tools and techniques. Miscellaneous. Design. Theory. Verification. Software engineering notes. 31, 1 (2006). FO UPD DENG-II Article