cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

language extension #190

Open ftc opened 7 years ago

ftc commented 7 years ago

after the paper is done:

Extend language to handle predicates over variables such as (l != null) or (l1 != l2)

Example usage:

This is needed since replacing a click listener on the button disables the old one. Without a predicate like this both setOnCLickLIsteners could be applied to the same concrete object at which point it would conflict with the enabling rule. setOnClickListener(l1) ; TRUE[*] ; setOnClickListener(l2 {l2 != l1}) |- l1.onClick(b)