##### Document Text Contents

Page 1

School of Computer Science and Engineering

The University of New South Wales

The Development of a Probabilistic B-Method

and a Supporting Toolkit

Thai Son Hoang

Bachelor of Engineering, UNSW

A thesis submitted for the degree of

Doctor of Philosophy

July 2005

Supervisor: Associate Professor Ken Robinson

Co-supervisor: Professor Carroll Morgan

Page 114

100 CHAPTER 5. PROBABILISTIC SPECIFICATION SUBSTITUTIONS

• Hoare triples [26]:

{P} S {Q} (5.2)

where P and Q are predicates over the program state, and S is program

statement. If P holds in the initial state and S is executed and terminates,

then Q is guaranteed to hold in the final state.

• Dijkstra’s weakest precondition [16]:

P ⇒ wp(S ,Q) (5.3)

where P and Q are predicates over the program state, and S is program state-

ment. The notation wp(S ,Q) denotes the weakest precondition of S with

respect to Q , i.e. the weakest precondition, under which Q is guaranteed to

be established after the execution of S .

• Morgan’s specification statements [43]:

v : [P ,Q ] (5.4)

where v is the frame, a sub-vector of the program variables whose values

may change. P and Q are predicates describing the initial state and the final

state, respectively.

Other notations also include Morris’s prescription [52] and Back’s pre/post-

condition specifications [8].

In B (or more precisely, GSL) [4], the same idea is presented with a different

syntax:

P | v : Q , (5.5)

with the meaning that the substitution will establish Q under the precondition P ,

and change only the variables in v . In this form, we will always assume that P

and Q are predicates over x and over x0, v , respectively. The variables v (sub-set

of the variables x ) are those that can be possibly changed by the substitution. The

variables x0 are distinct from x and represent their original values. Intuitively, the

meaning of (5.5) can be derived from the semantics presented Fig. 2.2 on page 12

by decomposing it into an unbounded choice substitution and a precondition sub-

stitution as follows:

P | @ v ′ ·

([

x0, v : = x , v

′]Q =⇒ v : = v ′) .

Page 115

5.2. PROBABILISTIC SPECIFICATION SUBSTITUTIONS 101

In fact, this is the form, into which the B-Toolkit will de-sugar the substitution.

It is common in B to get the meaning of a substitution by decomposing it in this

way. When this is done, it can be easily seen that specification (5.5) is just another

presentation of those illustrated in (5.2), (5.3) or (5.4).

5.2.2 Probabilistic Specification Substitutions

The ideas in Sec. 5.2.1 can be generalised to the probabilistic context. In this

section, we propose a probabilistic version of (5.5) which has the same role in the

probabilistic world as the original standard specification substitution does in the

standard world.

Recall that in the expectation logic, we write

A V [S ]B , (5.6)

to mean that the execution of S guarantees to establish that the expected value of

B over the final state distributions is bounded below by the value of A in the initial

state. By analogy with the connection between Dijkstra-style wp-specification and

Morgan’s specification statement, we propose a probabilistic specification substi-

tution written as in the standard case, that is

A | v : B , (5.7)

except that now A is an expectation defined over the program variables, B is an

expectation that may additionally refer to x0 and v . The variables v (which we also

call the frame of the substitution) are a sub-vector of program variables x , which

the substitution “constrains” to change only those variables (we will address what

we mean by constrains later).

As the first example, if we want to specify a coin that comes up heads with

probability at least one-half, then in the style of (5.6) we would write

1

2

V [Flip]〈coin = Head〉 ,

where coin is the state variable with possible values {Head ,Tail}. In the style of

(5.7), we would instead specify the substitution Flip as

1

2

| coin : 〈coin = Head〉 , (5.8)

Page 227

Appendix E

List of publications

Below are list of publications related to this dissertation.

1. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Probabilistic Invariants for Probabilistic Machines. In D. Bert,

J. P. Bowen, S. King, and M. Waldén, editors, ZB2003: Formal Specification

and Development in Z and B, Proceedings of the 3rd International Confer-

ence of B and Z Users, volume 2651 of Lecture Notes in Computer Science,

Turku, Finland, June 2003. Springer Verlag.

2. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Development via Refinement in Probabilistic B — Foundation

and Case Study. In Helen Treharne, Steve King, Martin Henson, and Steve

Schneider, editors, ZB2005: Formal Specification and Development in Z and

B, Proceedings of the 4th International Conference of B and Z Users, vol-

ume 3455 of Lecture Notes in Computer Science, pages 355–373, Guildford,

United Kingdom, April 2005. Springer Verlag.

3. Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Probabilistic ter-

mination in B. In D. Bert, J. P. Bowen, S. King, and M. Waldén, editors,

ZB2003: Formal Specification and Development in Z and B, Proceedings of

the 3rd International Conference of B and Z Users, volume 2651 of Lecture

Notes in Computer Science, Turku, Finland, June 2003. Springer Verlag.

4. Carroll Morgan, Thai Son Hoang, and Jean-Raymond Abrial. The Challenge

of Probabilistic Event-B. In Helen Treharne, Steve King, Martin Henson, and

213

Page 228

214 APPENDIX E. LIST OF PUBLICATIONS

Steve Schneider, editors, ZB2005: Formal Specification and Development

in Z and B, Proceedings of the 4th International Conference of B and Z

Users, volume 3455 of Lecture Notes in Computer Science, pages 162–171,

Guildford, United Kingdom, April 2005. Springer Verlag.

5. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A Case Study in pAMN. Technical report, Royal Holloway, the

University of London, 2003. CSD-TR-03-17.

6. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Electronic Notes in Theoretical Com-

puter Science (ENTCS), April 2005.

7. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Formal Aspects of Computing, 2005.

Submitted for publication.

School of Computer Science and Engineering

The University of New South Wales

The Development of a Probabilistic B-Method

and a Supporting Toolkit

Thai Son Hoang

Bachelor of Engineering, UNSW

A thesis submitted for the degree of

Doctor of Philosophy

July 2005

Supervisor: Associate Professor Ken Robinson

Co-supervisor: Professor Carroll Morgan

Page 114

100 CHAPTER 5. PROBABILISTIC SPECIFICATION SUBSTITUTIONS

• Hoare triples [26]:

{P} S {Q} (5.2)

where P and Q are predicates over the program state, and S is program

statement. If P holds in the initial state and S is executed and terminates,

then Q is guaranteed to hold in the final state.

• Dijkstra’s weakest precondition [16]:

P ⇒ wp(S ,Q) (5.3)

where P and Q are predicates over the program state, and S is program state-

ment. The notation wp(S ,Q) denotes the weakest precondition of S with

respect to Q , i.e. the weakest precondition, under which Q is guaranteed to

be established after the execution of S .

• Morgan’s specification statements [43]:

v : [P ,Q ] (5.4)

where v is the frame, a sub-vector of the program variables whose values

may change. P and Q are predicates describing the initial state and the final

state, respectively.

Other notations also include Morris’s prescription [52] and Back’s pre/post-

condition specifications [8].

In B (or more precisely, GSL) [4], the same idea is presented with a different

syntax:

P | v : Q , (5.5)

with the meaning that the substitution will establish Q under the precondition P ,

and change only the variables in v . In this form, we will always assume that P

and Q are predicates over x and over x0, v , respectively. The variables v (sub-set

of the variables x ) are those that can be possibly changed by the substitution. The

variables x0 are distinct from x and represent their original values. Intuitively, the

meaning of (5.5) can be derived from the semantics presented Fig. 2.2 on page 12

by decomposing it into an unbounded choice substitution and a precondition sub-

stitution as follows:

P | @ v ′ ·

([

x0, v : = x , v

′]Q =⇒ v : = v ′) .

Page 115

5.2. PROBABILISTIC SPECIFICATION SUBSTITUTIONS 101

In fact, this is the form, into which the B-Toolkit will de-sugar the substitution.

It is common in B to get the meaning of a substitution by decomposing it in this

way. When this is done, it can be easily seen that specification (5.5) is just another

presentation of those illustrated in (5.2), (5.3) or (5.4).

5.2.2 Probabilistic Specification Substitutions

The ideas in Sec. 5.2.1 can be generalised to the probabilistic context. In this

section, we propose a probabilistic version of (5.5) which has the same role in the

probabilistic world as the original standard specification substitution does in the

standard world.

Recall that in the expectation logic, we write

A V [S ]B , (5.6)

to mean that the execution of S guarantees to establish that the expected value of

B over the final state distributions is bounded below by the value of A in the initial

state. By analogy with the connection between Dijkstra-style wp-specification and

Morgan’s specification statement, we propose a probabilistic specification substi-

tution written as in the standard case, that is

A | v : B , (5.7)

except that now A is an expectation defined over the program variables, B is an

expectation that may additionally refer to x0 and v . The variables v (which we also

call the frame of the substitution) are a sub-vector of program variables x , which

the substitution “constrains” to change only those variables (we will address what

we mean by constrains later).

As the first example, if we want to specify a coin that comes up heads with

probability at least one-half, then in the style of (5.6) we would write

1

2

V [Flip]〈coin = Head〉 ,

where coin is the state variable with possible values {Head ,Tail}. In the style of

(5.7), we would instead specify the substitution Flip as

1

2

| coin : 〈coin = Head〉 , (5.8)

Page 227

Appendix E

List of publications

Below are list of publications related to this dissertation.

1. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Probabilistic Invariants for Probabilistic Machines. In D. Bert,

J. P. Bowen, S. King, and M. Waldén, editors, ZB2003: Formal Specification

and Development in Z and B, Proceedings of the 3rd International Confer-

ence of B and Z Users, volume 2651 of Lecture Notes in Computer Science,

Turku, Finland, June 2003. Springer Verlag.

2. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Development via Refinement in Probabilistic B — Foundation

and Case Study. In Helen Treharne, Steve King, Martin Henson, and Steve

Schneider, editors, ZB2005: Formal Specification and Development in Z and

B, Proceedings of the 4th International Conference of B and Z Users, vol-

ume 3455 of Lecture Notes in Computer Science, pages 355–373, Guildford,

United Kingdom, April 2005. Springer Verlag.

3. Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Probabilistic ter-

mination in B. In D. Bert, J. P. Bowen, S. King, and M. Waldén, editors,

ZB2003: Formal Specification and Development in Z and B, Proceedings of

the 3rd International Conference of B and Z Users, volume 2651 of Lecture

Notes in Computer Science, Turku, Finland, June 2003. Springer Verlag.

4. Carroll Morgan, Thai Son Hoang, and Jean-Raymond Abrial. The Challenge

of Probabilistic Event-B. In Helen Treharne, Steve King, Martin Henson, and

213

Page 228

214 APPENDIX E. LIST OF PUBLICATIONS

Steve Schneider, editors, ZB2005: Formal Specification and Development

in Z and B, Proceedings of the 4th International Conference of B and Z

Users, volume 3455 of Lecture Notes in Computer Science, pages 162–171,

Guildford, United Kingdom, April 2005. Springer Verlag.

5. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A Case Study in pAMN. Technical report, Royal Holloway, the

University of London, 2003. CSD-TR-03-17.

6. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Electronic Notes in Theoretical Com-

puter Science (ENTCS), April 2005.

7. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Formal Aspects of Computing, 2005.

Submitted for publication.