Some background: my project is to make a compiler that compiles from a c-like language to Alloy. The input language, that has c-like syntax, must support contracts. For now, I am trying to implement if statements that support pre and post condition statements, similar to the following:
int x=2
if_preCondition(x>0)
if(x == 2){
x = x + 1
}
if_postCondtion(x>0)
The problem is that I am a bit confused with the results of Alloy.
sig Number{
arg1: Int,
}
fun addOneConditional (x : Int) : Number{
{ v : Number |
v.arg1 = ((x = 2 ) => x.add[1] else x)
}
}
assert conditionalSome {
all n: Number| (n.arg1 = 2 ) => (some field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] })
}
assert conditionalAll {
all n: Number| (n.arg1 = 2 ) => (all field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] })
}
check conditionalSome
check conditionalAll
In the above example, conditionalAll does not generate any Counterexample. However, conditionalSomegenerates Counterexamples. If I understand all and some quantifiers correctly then there is a mistake. Because from mathematical logic we have Ɐx expr(x) => ∃x expr(x) ( i.e. If expression expr(x) is true for all values of x then there exist a single x for which expr(x) is true)
The first thing is that you need to model your pre-, post- and operations. Functions are terrible for that because they cannot not return something that indicates failure. You, therefore, need to model the operation as a predicate. The value of a predicate indicates if the pre/post are satisfied, the arguments and return values can be modeled as parameters.
This is as far as I can understand your operation:
pred add[ x : Int, x' : Int ] {
x > 0 -- pre condition
x = 2 =>
x'=x.plus[1]
else
x'=x
x' > 0 -- post condition
}
Alloy has no writable variables (Electrum has) so you need to model the before and after state with a prime (') character.
We can now use this predicate to calculate the set of solutions to your problem:
fun solutions : set Int {
{ x' : Int | some x : Int | add[ x,x' ] }
}
We create a set with integers for which we have a result. The prime character is nothing special in Alloy, it is only a convention for the post-state. I am abusing it slightly here.
This is more than enough Alloy source to make mistakes so let's test this.
run { some solutions }
If you run this then you'll see in the Txt view:
skolem $solutions={1, 3, 4, 5, 6, 7}
This is as expected. The add operation only works for positive numbers. Check. If the input is 2, the result is 3. Ergo, 2 can never be a solution. Check.
I admit, I am slight confused by what you're doing in your asserts. I've tried to replicate them faithfully, although I've removed unnecessary things, at least I think we're unnecessary. First your some case. Your code was doing an all but then selecting on 2. So removed the outer quantification and hardcoded 2.
check somen {
some x' : solutions | 2.plus[1] = x'
}
This indeed does not give us any counterexample. Since solutions was {1, 3, 4, 5, 6, 7}, 2+1=3 is in the set, i.e. the some condition is satisfied.
check alln {
all x' : solutions | 2.plus[1] = x'
}
However, not all solutions have 3 as the answer. If you check this, I get the following counter-example:
skolem $alln_x'={7}
skolem $solutions={1, 3, 4, 5, 6, 7}
Conclusion. Daniel Jackson advises not to learn Alloy with Ints. Looking at your Number class you took him literally: you still base your problem on Ints. What he meant is not use Int, don't hide them under the carpet in a field. I understand where Daniel is coming from but Ints are very attractive since we're so familiar with them. However, if you use Ints, let them at least use their full glory and don't hide them.
Hope this helps.
And the whole model:
pred add[ x : Int, x' : Int ] {
x > 0 -- pre condition
x = 2 =>
x'=x.plus[1]
else
x'=x
x' > 0 -- post condition
}
fun solutions : set Int { { x' : Int | some x : Int | add[ x,x' ] } }
run { some solutions }
check somen { some x' : solutions | x' = 3 }
check alln { all x' : solutions | x' = 3 }