pacti-org / pacti

A package for compositional system analysis and design
https://www.pacti.org
BSD 3-Clause "New" or "Revised" License
19 stars 5 forks source link

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

Open iincer opened 10 months ago

iincer commented 10 months ago

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.