What people are saying - Write a review
We haven't found any reviews in the usual places.
A Relational Approach
Program verification and construction
12 other sections not shown
Other editions - View all
1-correct 1-recoverable array asserted program backward error recovery begin b1 binary relations boolean cartesian product Chapter characterizations Compute computes function consider correct with respect critical information deduce defined definition denoted determinacy deterministic discrete mathematics discuss dom(fl dom(i domain element end end Equation equivalence equivalence relation error detection Example executable assertions Exercises 1[A expected function expression following relations following specification formula forward error recovery FTR'm FTRm functional abstraction given greatest common divisor Hence heuristic initial state s0 input integer end iteration label loose correctness loosely recoverable max(s maximal element message(1 milestone min(s more-defined non-deterministic output Pascal past path predicate predicate-based preserved procedure program fault tolerance program on space Proof Proposition PSTm recovery block recovery routine reference to Exercises regular relations relational product representationally Section sp-correct sp-recoverable specificationwise statement strict correctness strict partial ordering structured programming subset sum(s transitive closure valid variables