Programs, Recursion and Unbounded Choice
Programs, Recursion and Unbounded Choice This book is a complete account of the predicate transformation calculus semantics of sequential programs, including repetitions, recursive procedures,…
Specifikacia Programs, Recursion and Unbounded Choice
Programs, Recursion and Unbounded Choice
This book is a complete account of the predicate transformation calculus semantics of sequential programs, including repetitions, recursive procedures, computational induction and unbounded nondeterminacy. The author develops this theory to a greater depth than has been achieved before, and describes it in a way that makes it readily compatible with programming rules for partial and total correctness of repetitions and recursive procedures, supplies new rules for proving incorrectness, and a stronger rule for proving that two programs satisfy the same specifications. Predicate transformation semantics are the best specification method for the development of correct and well-structured computer programs.
This will be essential reading for all computer scientists working in specification and verification of programs. Finally, the semantics are extended so that non-terminating programs can be specified as well.