specifying addition on floating-point values

[mohittkr]

Hello,

I am new to GOSPEL. I am trying to define a logic function on floating-point addition:

(*@ function add (x y: float) : float = 
        Float.add x y *)

I used OCaml's Float.add for adding two floating-point numbers. Is it okay to use Float.add or is there an addition operation defined in GOSPEL standard library.

I get the following error when doing gospel check:
Error: Type checking error: no module with name Float or file with name float.mli

I am not sure how to get around this error.

[n-osborne]

Thank you for your question.

You can't use an OCaml function in the logical space except if it is annotated with the pure keyword in its Gospel specification. And the OCaml standard library is not specified at the moment.
What you can use is the Gospel standard library, but it does not contain any float type or operation.
If you want to talk about floating-point operations, one way that I can think of is to give a Gospel model to the float type and then describe how operation should behave in respect to this model.