Topic: predicate transforms

topics > computer science > programming > Group: program proving

program proof via assertions
programming as mathematics
requirement specification by assertion


Dijkstra treats program instructions as predicate transforms acting upon relational conditions. He specifies required relationships for program termination and inverts each instruction's transform to find the weakest pre-condition needed at program initiation. If the programmer can satisfy this pre-condition then the program is correct. Other workers have expanded on his techniques. For instance Redelmeier (QuoteRef: redeDH7_1979) has developed a recursive refinement language removing the need for looping and variables. (cbb 5/80)
Subtopic: predicate transforms up

Quote: the transformed predicate is the weakest precondition that gives the original predicate after execution [»parnDL10_1976]
QuoteRef: parnDL10_1976 ;;6 Dijkstra's predicate transforms show previous state given state and just executed instruction
QuoteRef: parnDL10_1976 ;;3 using predicate transforms for program proof reason backwards through the program this is more accurate and a better double check of program
QuoteRef: parnDL10_1976 ;;9 predicate transform for assignment is T[X:=E] = | P(x)->P(E) |
Quote: example of applying a predicate transform to a while program; also need termination [»parnDL10_1976]

Subtopic: precondition and postcondition up

Quote: example of the weakest precondition for a simple assignment statement [»redeDH7_1979]
Quote: a postcondition is true after a statement; the canonical postcondition most restricts the state

Related Topics up

Topic: program proof via assertions (61 items)
Topic: programming as mathematics (27 items)
Topic: requirement specification by assertion
(28 items)

Updated barberCB 11/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.