[SMT-LIB] Translation of JML predicate into SMT language

[Claude Marche]

Daniela da Cruz wrote:
> Hello.
>
> I am trying to translate the *\sum* predicate from JML into SMT language,
> but I had no sure that I am going in the right way
> and probably here someone can help me.
>
> One example of this predicate, would be:
>
> \sum int i; 0 <= i && i < n; a[i])
>
> My first try to translate it into SMT (just for arrays, for now) resulted in
> something like this:
>
> :extrafuns ((sum_predicate Int Int Array Int))
> :assumption (forall (?i Int) (= (sum_predicate ?i ?i ?a) (select ?a ?i)))
> :assumption (forall (?i Int) (?j Int) (?a Array) (= (sum_predicate ?i ?j ?a)
> (+ (select ?a ?i) (sum_predicate (+ ?i 1) ?j ?a))))
>
> However, I think that is very slow. Also, how I would write this in version
> 2.0?
>   
I don't understand what you mean by "very slow."

The first step should be to make the axiomatization sound. It seems to
me that your second axiom requires an hypothesis i < j

you could add more axioms, e.g.

i > j implies sum(i,j,a) = 0

and

i <= j <=k implies sum(i,k,a) = sum(i,j,a)+sum(j,k,a)

This might help the provers.

- Claude


-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Saclay - Île-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Université                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |