Hi,
thanks a a lot, this looks like it's gonna help me.
cheers!
On Fri, May 4, 2018 at 11:08 AM, Claude Marché <claude.mar...@inria.fr>
wrote:
> Please find in attachment a more complete example file mlw.ml that
> includes the construction of the small program
>
> let f (a:array int)
> requires { a.length >= 1 }
> ensures { a[0] = 42 }
> = a[0] <- 42
>
> Hope this helps,
>
> Le 02/05/2018 à 22:20, Gian Pietro Farina a écrit :
>
>> Hi, and thanks for the reply.
>> Sorry if my questions sound naive.
>>
>> I've now read that part of the manual and I can now load the module Array.
>> But I have some difficulties, for instance:
>> I am trying to build formulas and terms such as a[0]>1 /\ a[1]>2 ==>
>> a[0]+a[1]>3 .
>> I fail though in even understanding how to build a term of type "array".
>> While for "first order" terms like integers or naturals it works ok.
>> I would also eventually like to quantify existentially over a its indices.
>> I m trying to read this http://why3.lri.fr/stdlib-0.81/array.mlw.html
>> but I don't understand how to do things in ocaml.
>>
>>
>> Cheers,
>> GP
>>
>>
>> On Wed, May 2, 2018 at 5:37 AM, Claude Marché <claude.mar...@inria.fr
>> <mailto:claude.mar...@inria.fr>> wrote:
>>
>>
>> Hello,
>>
>> I guess you already read the chapter 4 of the manual
>> (http://why3.lri.fr/doc/api.html#sec30
>> <http://why3.lri.fr/doc/api.html#sec30>). The importation of
>> modules and the manipulation of programs is not documented yet,
>> but you can find some examples of use in the directory
>> examples/use_api of the distribution: files mlw.ml <http://mlw.ml>
>> and mlw_tree.ml <http://mlw_tree.ml>.
>>
>> Indeed there is a subtle distinction between modules and theories.
>> Arrays are in a module and not in a theory. Specifically, the
>> importation of a module is done using Mlw_module.read_module. see
>> http://why3.lri.fr/api/Mlw_module.html
>> <http://why3.lri.fr/api/Mlw_module.html>
>>
>> Do not hesitate to request for more help on any specific use of
>> the API
>>
>> - Claude
>>
>>
>>
>> Le 01/05/2018 à 23:55, Gian Pietro Farina a écrit :
>>
>> Hello,
>>
>> I would like to use the Ocaml api of why3 in my project where
>> I need to send to the smt solvers
>> queries in the theory of arrays. How do I load a theory in my
>> project?
>>
>> Best regards,
>> Gian Pietro
>>
>>
>>
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> <mailto:Why3-club@lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>> <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
>>
>>
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> <mailto:Why3-club@lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>> <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
>>
>>
>>
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
