| 
|
Topic: predicate transforms
topics >
computer science >
programming >
program proof via assertions
Topic:
programming as mathematics
Topic:
requirement specification by assertion
Summary
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: precondition and postcondition
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]
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
[»redeDH7_1979]
Topic: program proof via assertions (61 items)
Topic: programming as mathematics (27 items)
Topic: requirement specification by assertion
(28 items)