Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/161030
9 Visitors
11 Hits
0 Downloads
- Title
- Development via refinement in probabilistic B — foundation and case study
- Related
- International Conference of B and Z Users (4th : 2005) (13 - 15 April 2005 : Guildford, England)
- Related
- Treharne, Helen; King, Steve; Henson, Martin and Schneider, Steve;. ZB 2005 : formal specification and development in Z and B : 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005 : proceedings, p.355-373
- DOI
- 10.1007/11415787_21
- Related
- Lecture notes in computer science Vol. 3455
- Publisher
- Berlin : Springer Verlag
- Date
- 2005
- FoR/RFCD Code(s)
-
080300 Computer Software
- Author/Creator
- Hoang, Thai Son
- Author/Creator
- Jin, Zhendong
- Author/Creator
- Robinson, Ken
- Author/Creator
- McIver, Annabelle
- Author/Creator
- Morgan, Carroll
- Description
- In earlier work, we introduced probability to the 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.
- Description
- 19 page(s)
- Subject Keyword
- 080300 Computer Software
- Subject Keyword
- probability
- Subject Keyword
- program correctness
- Subject Keyword
- generalised substitutions
- Subject Keyword
- weakest preconditions
- Subject Keyword
- B
- Subject Keyword
- randomised algorithms
- Subject Keyword
- refinement
- Resource Type
- conference paper
- Organisation
- Macquarie University. Dept. of Computing
- Identifier
- http://hdl.handle.net/1959.14/161030
- Identifier
- ISBN:9783540255598
- Identifier
- ISSN:0302-9743
- Identifier
- mq-rm-2005003316
- Language
- eng
- Reviewed
