Using Z Specification, Refinement, and Proof

Livro digital

Título:
Using Z Specification, Refinement, and Proof

Autor:
Jim Woodcock, Jim Davies

Categoria:
Tecnologia > Geral

Doador:
Raffaello D. N.

Sinopse:
Formal methods promise software we can reason about, yet the mathematical machinery behind them often feels out of reach for working engineers. This book meets that gap head-on: it introduces the Z notation through the lens of the CICS experience, where formal specification uncovered subtle errors in a large transaction-processing system, and builds the case for abstraction and proof as practical engineering tools rather than academic ceremony. The first part assembles the mathematical toolkit step by step, moving from propositional and predicate logic through equality, sets, relations, functions, sequences and free types. Each concept is then folded into Z's schema calculus, covering schema operators, promotion and preconditions, so the notation becomes a coherent language for describing state, operations and invariants of a system. The closing chapters turn to refinement and proof, with data refinement, functional refinement and the refinement calculus illustrated through worked industrial case studies: a file system, a telecommunications protocol, an operating system scheduler, a bounded buffer and a save area. The result is a complete route from abstract specification to provably correct implementation, valuable both as a self-contained course in Z and as a reference for practitioners in formal methods and software verification.