Support arbitrary invertible action relations

[viper-admin]

Created by @mschwerhoff on 2018-02-15 16:14 Last updated on 2018-03-05 12:29

The general syntax of actions is the following:

?x1, ?x2, ... | c(x1, ...) | G(g1(x1, ...), g2(x1, ...), ...): e(x1, ...) ~> e'(x1, ...)

where c, gᵢ, e and e' are expressions that can mention the bound variables. Checking that a performed state change is allowed means asserting that there exist appropriate xᵢ, which in practice is typically impossible for SMT solvers.

A trick to avoid existentials is to use inverse functions, but that isn't implemented yet. Instead, Voila currently only supports a few special cases of invertible actions: those, where the bound variables directly constitute at least one of the expressions gᵢ, e or e'.

Supported examples are:

G: 0 ~> 1
?n | 0 <= n <= 1 | G: n ~> 3*n
?n, ?m | n < m | G: n ~> m
?n, ?m, ?k | n < m | G(k): n ~> m

Not yet supported examples are:

?n | G: 3*n ~> 3*n+1
?n, ?m | G: n+m ~> n-m   // not transitively closed anyway
n, ?m, ?k | n < m | G(3*k): n ~> m
?xs, ?x | G: xs ~> xs union Set(x)

[viper-admin]

@mschwerhoff on 2018-02-15 16:14:

• edited the title

[viper-admin]

@mschwerhoff commented on 2018-02-15 16:25

First step: properly reject unsupported programs, instead of crashing

[viper-admin]

@mschwerhoff on 2018-03-05 12:29:

• edited the description