Development via refinement in probabilistic B - Foundation and case study

Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

In earlier work, we introduced probability to the B-Method (B) by providing a probabilistic choice substitution and by extending B 's semantics to incorporate its meaning [8], This, a first step, allowed probabilistic programs to be written and reasoned about within B. This paper extends the previous work into refinement within B. To allow probabilistic specification and development within B, we must add a probabilistic specification substitution; and we must determine the rules and techniques for its rigorous refinement into probabilistic code. Implementation in B frequently contains loops. We generalise the standard proof obligation rules for loops giving a set of rules for reasoning about the correctness of probabilistic loops. We present a small case-study that uses those rules, the randomised Min-Cut algorithm.

Original languageEnglish
Pages (from-to)355-373
Number of pages19
JournalLecture Notes in Computer Science
Volume3455
Publication statusPublished - 2005

Fingerprint Dive into the research topics of 'Development via refinement in probabilistic B - Foundation and case study'. Together they form a unique fingerprint.

  • Cite this