pacti-org/pacti

[BUG] Some contract compositions yield guarantees that only involve inputs

Opened this issue · 0 comments

iincer commented

Describe the bug
Consider the composition of the following contacts:

C1 = {
inputs: a
outputs: b
assumptions: a < 2
guarantees: b = a, b < 2
}

C2 = {
inputs: b
outputs: c
assumptions: b < 1
guarantees: c = b
}

The composition could generate the guarantee a < 2. This guarantee should not be there. Or is this a sympthom of a problematic specification?

Expected behavior
Pacti should not generate guarantees that only use input variables.