- Full Description
The book is a focused survey on probabilistic program semantics, conceived to tell a coherent story with a uniform notation. It is grouped into three themes: Part I is for 'users' of the techniques who will be developing actual programs; Part II gives mathematical foundations intended for those studying exactly how it was done and how to build semantic structures/models in their own work; and Part III describes a very 'hot' research direction, temporal logic and model checking. Topics and features: - introduces readers to very up-to-date research in the mathematics of rigorous development of randomized (probabilistic) algorithms - illustrates by example the typical steps necessary in computer science to build a mathematical model of any programming paradigm - presents results of a large and integrated body of research in the area of 'quantitative' program logics An advanced research survey monograph, integrating three major topic areas: random/probabilistic algorithms, assertion-based program reasoning, and refinement programming models. Essential foundation topic for modern sequential programming methodology.
- Table of Contents
Table of Contents
- Introduction to pGCL.
- Invariants and variants for probabilistic loops.
- Case studies in termination .
- Probabilistic data refinement.
- Theory for the demonic model.
- Geometry of probabilistic programs.
- Proven rules for probabilistic loops.
- Transformer hierarchy.
- Quantitative temporal logic qTL.
- Quantitative algebra of qTL.
- Quantitative modal u
- calculus of qMu, and games.
Please Login to submit errata.No errata are currently published