Currently, specification elements are represented in the WyIL file format as Tuple<Expr>. This is actually quite limited for several reasons:
Modifiers. We cannot have public / private specification elements, etc. Similarly, synthetic elements which have been inferred.
Queries. For a given expression, we cannot ask a question like: is this expression within a specification element?
Therefore, it makes sense to me to have a specific type such that Tuple<Expr> becomes Tuple<Element> (or similar) where Element wraps the Expr. Perhaps it makes sense even to distinguish Where, Requires, Ensures.
Currently, specification elements are represented in the WyIL file format as
Tuple<Expr>. This is actually quite limited for several reasons:Therefore, it makes sense to me to have a specific type such that
Tuple<Expr>becomesTuple<Element>(or similar) whereElementwraps theExpr. Perhaps it makes sense even to distinguishWhere,Requires,Ensures.