Add support for describing variables.

[NicolasRouquette]

Instead of using comments to describe contract variables, it would be useful to keep track of the description in the variable object.

That is, instead of the constructor:

class Var:
    """
    Variables used in system modeling.

    Variables allow us to name an entity for which we want to write constraints.
    """

    def __init__(self, varname: str):
        self._name = str(varname)

We should have something like this:

class Var:
    """
    Variables used in system modeling.

    Variables allow us to name an entity for which we want to write constraints.
    """

    def __init__(self, varname: str, description: Optional[str] = None):
        self._name = str(varname)
        self._description = str(description)

It would be useful to show this description in Pacti's error messages. For example, the IoContract constructor raises an error when variables appear in inputs and outputs. For such error messages, it would be helpful to show the associated variable description, if any.

[iincer]

Absolutely, this would be a lightweight means of supporting something close to a natural language output for contracts.

It immediately comes to mind that we could extend Term with an identifier. When Pacti computes a term using others, it could in principle keep track of what terms were used to derive a system-level spec or a quotient. This could add a great deal of traceability to computed specifications.

[NicolasRouquette]

Indeed! Just to confirm that we're on the same page, the idea is to define a constructor for Term like this:

class Term(ABC):
   def __init__(self, id: Optional[str] = None):
      self._id = id

Then, we'd have to add a similar constructor argument to PolyhedralTerm like this:

class PolyhedralTerm(Term):
    def __init__(self, variables: dict[Var, numeric], constant: numeric, id: Optional[str]=None):
        super().__init__(id)
        # ...

[iincer]

Exactly! 😃

[NicolasRouquette]

Consider the following example from the space_mission case study:

def SBO_contract(s: int, duration: float, generation: float, consumption: float, improvement: float) -> tuple[int, PolyhedralContract]:
  e = s+1
  spec = PolyhedralContract.readFromString(
    InputVars = [
      f"t{s}",    # Scheduled start time
      f"soc{s}",  # initial battery SOC
      f"d{s}",    # initial data volume
      f"e{s}",    # initial trajectory error
      f"r{s}",    # initial relative distance
    ],
    OutputVars = [
      f"t{e}",    # Scheduled end time
      f"soc{e}",  # final battery SOC
      f"d{e}",    # final data volume
      f"e{e}",    # final trajectory error
      f"r{e}",    # final relative distance
    ],
    assumptions = [
      # Battery has enough energy for the consumption over the duration of the task instance
      f"-soc{s} <= -{duration*consumption}",
    ],
    guarantees = [
      # Scheduled task instance end time
      f"t{e} - t{s} = {duration}",
    
      # Battery discharges by at most duration*consumption
      f"soc{s} - soc{e} <= {duration*consumption}",

      # data volume increases by at least duration*generation
      f"d{s} - d{e} <= -{duration*generation}",

      # trajectory error improves by at least duration*improvement
      f"e{s} - e{e} <= -{duration*improvement}",

      # no change to relative distance
      f"r{e} - r{s} = 0",
    ])
  return e, spec

This raises some questions:

• What is the syntax for specifying a variable name and description?
• What is the syntax for specifying a term constraint and id?
• Should we also consider supporting a term description as well as id and if so, what would be the syntax for it?

[NicolasRouquette]

Also, we would need a scheme for generating IDs when we apply term rewriting.

For example, rule 4 rewrites:

LHS = RHS

into:

LHS <= RHS
-(LHS) <= -(RHS)

Suppose ID is the identifier for the original term, LHS = RHS, we should generate new identifiers for the 2 resulting terms; e.g., ID (rule4.pos) and ID (rule4.neg) or something shorter.

[iincer]

What is the syntax for specifying a variable name and description?

Currently, we only have the notion of a name for a variable--it serves as its ID. This is a string. The name is used to know how we connect contracts to each other. A description could be an arbitrary string that gives an explanation for a variable, e.g.,
f"t{s}", # Scheduled start time
I don't see a reason to limit what the user could write. What benefits do you see?

What is the syntax for specifying a term constraint and id?
Should we also consider supporting a term description as well as id and if so, what would be the syntax for it?

An ID could be generated by Pacti or given by the user as a string. A description could be given by the user as a sentence (e.g., "requirement E57 of standard IEEE AAA.BBB v1.2").
To support #146, it may make sense for every requirement to contain a list of IDs of terms on which it depends.

Also, we would need a scheme for generating IDs when we apply term rewriting.

This is true also after performing contract computations. For the moment, we could gave a generate_term_id(list_of_terms, number_of_ids) function somewhere that takes as input the IDs that generate this contract and the number of IDs to generate. This function would be used by the parser to assign new IDs and by the polyhedral operations when generating new terms.