CodePlexProject Hosting for Open Source Software

1

Vote
Please consider the following auxiliary module:

If there is no extends statement, the step <2> can be proven.

If we extend from Integers, TLAPS, we obtain the following obligation for <2>:

This behaviour is also quite fragile: changing A(x,magicValue) to A(magicValue) makes the bug disappear. Likewise, if we remove the SUFFICES step and use the same argument for the outer proof(the statement is the same after narrowing the problem down), the bug also disappears.

```
------------------------- MODULE miniAbstractPaxos -------------------------
\* uncomment all extends, to let the theorem Abstraction in minimal go through
\* EXTENDS TLAPS, Integers \* use this and v will unfold to LAMBDA magicBallot, magicValue : TRUE
\* EXTENDS Integers, TLAPS \* use this and v will unfold to LAMBDA magicBallot, magicValue, x1, x2 : x1 + x2
EXTENDS TLAPS \* use this and v will unfold to A!SMT
VARIABLES maxVal
AbsInit == maxVal = [a \in {} |-> "null"]
=====
```

which defines the Operator AbsInit and the variable maxVal. We now define a parametrized instance A(x, magicValue) where we instanciate maxVal with a dummy operator dependent on magicValue:```
------------------------------ MODULE minimal ------------------------------
CONSTANTS C,D
absMaxVal(magicValue) == {}
A(x,magicValue) ==
INSTANCE miniAbstractPaxos WITH
maxVal <- absMaxVal(magicValue)
THEOREM Abstraction ==
ASSUME NEW v
PROVE TRUE
<1>1. TRUE
<2>. SUFFICES ASSUME TRUE PROVE A(v,v)!AbsInit
<2>4. absMaxVal(v) = [a \in C |-> "null"]
<2>. QED BY <2>4 DEF A!AbsInit
<1>. QED
====
```

Then the obligation depends on the extends statement in miniAbstractPaxos: If there is no extends statement, the step <2> can be proven.

If we extend from Integers, TLAPS, we obtain the following obligation for <2>:

```
ASSUME NEW CONSTANT C,
NEW CONSTANT D,
NEW CONSTANT v,
TRUE ,
absMaxVal(v) = [a \in C |-> "null"]
PROVE absMaxVal(LAMBDA x, magicValue, x1, x2 : x1 + x2)
= [a \in {} |-> "null"]
```

If we remove extend TLAPS first and then Integers, we obtain:```
ASSUME NEW CONSTANT C,
NEW CONSTANT D,
NEW CONSTANT v,
TRUE ,
absMaxVal(v) = [a \in C |-> "null"]
PROVE absMaxVal(LAMBDA x, magicValue : TRUE) = [a \in {} |-> "null"]
```

And if we extend only TLAPS, we obtain:```
ASSUME NEW CONSTANT C,
NEW CONSTANT D,
NEW CONSTANT v,
TRUE ,
absMaxVal(v) = [a \in C |-> "null"]
PROVE absMaxVal(A!SMT) = [a \in {} |-> "null"]
```

In all cases, v should not be expanded to anything, since it is a new variable (and even if it were an operator, it needed to be contained in the BY DEF statement).
This behaviour is also quite fragile: changing A(x,magicValue) to A(magicValue) makes the bug disappear. Likewise, if we remove the SUFFICES step and use the same argument for the outer proof(the statement is the same after narrowing the problem down), the bug also disappears.

## comments