What people are saying - Write a review
We haven't found any reviews in the usual places.
MODELS OF COMPUTATION
APPROACHES TO PROOFS OF PARTIAL CORRECTNESS
6 other sections not shown
abstract data type abstract machine abstract model specification abstract program algebraic specification algorithm applied array auxiliary variables axiomatic approach axiomatic method axioms behavior calculus cobegin coend correctness proof data objects deductive system defined definition Demonstration denote effect establish example execution function formal methods formal specification given h depth Hence implementing programs inductive assertion method inference rules initial state d0 input integer intermediate assertions iseq iterative constructs loop invariant multiset noninterference nullseq operations parallel programs partial correctness pointer postcondition precondition Q predicate transformer program construction program semantics program verification programming language prove requires result rule of consequence s-unit Section sequence sequential proofs set of legitimate specification language stack level state-machine specification syntactic technique termination theory tion total correctness true underflow underlying abstraction V-function valid verification condition vfun weakest precondition wp transformers wp(j