Provides an integrated coverage of random/probabilistic algorithms, assertion-based program reasoning, and refinement programming models, providing a focused survey on probabilistic program semantics. This book illustrates, by examples, the typical steps necessary to build a mathematical model of any programming paradigm.
Abstract:
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. Read more...
Author(s): McIver, Annabelle; Morgan, Charles C
Series: Monographs in computer science
Publisher: Springer New York
Year: 2005
Language: English
Pages: 397
Tags: Engineering mathematics.;Probabilities.;Systems engineering.
Content: Probabilistic guarded commands and their refinement logic.- to pGCL: Its logic and its model.- Probabilistic loops: Invariants and variants.- Case studies in termination: Choice coordination, the dining philosophers, and the random walk.- Probabilistic data refinement: The steam boiler.- Semantic structures.- Theory for the demonic model.- The geometry of probabilistic programs.- Proved rules for probabilistic loops.- Infinite state spaces, angelic choice and the transformer hierarchy.- Advanced topics: Quantitative modal logic and game interpretations.- Quantitative temporal logic: An introduction.- The quantitative algebra of qTL.- The quantitative modal ?-calculus, and gambling games.
