Is your feature request related to a problem? Please describe.
composition, quotient, and merging are binary contract operations that produce a new contract.
refinement is a binary boolean operation.
Describe the solution you'd like
In all 4 cases, we need information explaining the result.
For the 3 binary contract operations, an explanation involves:
explaining why the result variables (inputs, outputs) are what they are w.r.t. the original contracts;
explaining how each resulting assumption/guarantee constraint derives from a chain of operations, such as variable elimination by refinement vs. relaxation and simplification, all the way to the original contract constraints. This explanation bottoms at the invocation of tactics.
For the refinement operation, an explanation involves showing the individual constraint checks.
In all 4 cases, we need to provide explanations for both operation success and failure.
Success and failure explanations are important to assess whether there are any superfluous variables/constraints in the contracts and which tactics were involved in producing the result. This could be useful for developing specialized tactics and for identifying the need for new tactics.
Describe alternatives you've considered
A clear and concise description of any alternative solutions or features you've considered.
Additional context
Add any other context or screenshots about the feature request here.
Is your feature request related to a problem? Please describe.
composition, quotient, and merging are binary contract operations that produce a new contract. refinement is a binary boolean operation.
Describe the solution you'd like
In all 4 cases, we need information explaining the result.
For the 3 binary contract operations, an explanation involves:
For the refinement operation, an explanation involves showing the individual constraint checks.
In all 4 cases, we need to provide explanations for both operation success and failure.
Success and failure explanations are important to assess whether there are any superfluous variables/constraints in the contracts and which tactics were involved in producing the result. This could be useful for developing specialized tactics and for identifying the need for new tactics.
Describe alternatives you've considered A clear and concise description of any alternative solutions or features you've considered.
Additional context Add any other context or screenshots about the feature request here.