[SMT-LIB] SMT: arrays doubt

[Claude Marché]

Daniela da Cruz wrote:
> Hello all.
> I'm relatively new in SMT and I'm studying the arrays.
> However, when I have been looking for the Swap implementation (in Java+JML),
> I saw that it makes use of the method "length" defined
> by Java language.
> Can anyone tell me how this is translated to SMT? And how it supposed to
> translate something like "arr[i]"? Should I use some specific theory?

Translation of Java/JML constructs like the length method for arrays is 
not a concern of SMT provers but a concern of front-end tools which 
performing VC generation. Each of such tools has its one interpretation 
of it, in essence, something like arr[i] is translated into

   select(Heap,ptr_shift(arr,i))

where Heap is an array representing the memory, and ptr_shift(arr,i) is 
a representation of shifting reference arr with offset i (aka pointer 
arithmetic). select is the access function to arrays in classical SMT 
theory of arrays

I guess this question should go to the JML mailing list...

- 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                    |