cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

Add alias for regular expression #175

Closed smover closed 7 years ago

smover commented 7 years ago

In the current development of the specification @ftc notice that different rules always share the same common subexpressions.

For example, the expression used to check if a view is attached is used in several rules and is, modulo the naming of the variables, used in different rules.

This makes writing and maintaining the rules time consuming and error prone (e.g. if a small bug is found in one of these common subexpression, all of them must be changed).

Also, having a "name" for these subexpression may be more convenient (i.e. the name abstracts the concept and the complexity of the subexpression).

A solution to improve the issue is to allow "named" regular expressions in the language. For example:

NAMED_EXPR PRED1(l,v) := [CB] [ENTRY] [l] void view.onClick(v : View)

Then, the name can be used either inside another named expression or in a specification. For example:

SPEC PRED(l,v); [CI] [ENTRY] [b] boolean view.setVisible(true) |- ...