[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.