The Synthesis of Loop Predicates

Current methods for mechanical program verification
require a complete predicate specification 
on each loop.  Because this is tedious and error prone,
producing a program with complete, correct predicates 
is reasonably difficult and would be facilitated by machine
assistance.  This paper discusses techniques 
for mechanically synthesizing loop predicates.  Two classes
of techniques are considered: (1) heuristic 
methods which derive loop predicates from boundary conditions
and/or partially specified inductive assertions: 
(2) extraction methods which use input predicates and
appropriate weak interpretations to obtain certain 
classes of loop predicates by an evaluation on the weak interpretation.

CACM March, 1974

Wegbreit, B.

program verification, loop predicates, inductive
assertions, synthesis of loop predicates, weak 
interpretations, well-founded sets, property extraction, theorem proving

3.64 4.19 4.22 5.24

CA740206 JB January 18, 1978  12:55 PM 

2683	5	2683
2683	5	2683
2683	5	2683
2874	5	2683
3104	5	2683
1682	6	2683
2227	6	2683
2317	6	2683
2457	6	2683
2683	6	2683
2683	6	2683
2871	6	2683
521	6	2683