What people are saying - Write a review
We haven't found any reviews in the usual places.
A Recursion Removal Theorem
Demonstrating the Compliance of Ada Programs with
12 other sections not shown
Other editions - View all
abstract data types algorithm allow application assertion assignment auxiliary variables behaviour binary Boolean busy-waiting C. A. R. Hoare component Computer Science concrete confidentiality specification construction context correct data refinement data type deadlocked DecTree defined definition denotes derivation described Dijkstra event example executable expression finite formal methods formula function functor goal gray code guar implementation initial introduced invariant kernel lemma logic loop loop invariant machine metavariables module Morgan notation operation paper postcondition precondition predicate primed problem proc program refinement programming language Prolog proof obligations proof rule properties prove PV-segment recursive refinement calculus refinement rule refinement step refinement tree Reftree reification relation result rewriting satisfies secure semantics semaphore sequence specification statement st(rs stack subgoal subwindow synchroniser syntactic tactic termination theorem theory tion transformation transition true validity condition window inference window rule