Stream: Coq users

Topic: ✔ Trying to write specification of function (VST)


view this post on Zulip Lessness (Aug 03 2023 at 08:07):

Yes, thank you both.

@Michael Soegtrop I actually started the material yesterday and I have big hopes. :)

view this post on Zulip Lessness (Aug 03 2023 at 08:48):

Current specification is such (and it seems okay for my noob eyes):

Definition factorize_spec: ident * funspec :=
DECLARE _factorize
  WITH gv: globals, n: Z, f: Z, h: Z
  PRE [ tulong, tulong ]
    PROP (2 <= n <= Int64.max_signed; 2 <= f <= Int64.max_unsigned)
    PARAMS (Vlong (Int64.repr n); Vlong (Int64.repr f))
    SEP (data_at Ews tulong (Vlong (Int64.repr h)) (gv _highest))
  POST [ tulong ]
    PROP ()
    RETURN (Vlong (Int64.repr (repeated_div f n)))
    SEP (data_at Ews tulong (Vlong (Int64.repr (new_highest f n h))) (gv _highest)).

view this post on Zulip Notification Bot (Aug 03 2023 at 08:49):

Lessness has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (Aug 03 2023 at 09:43):

I don't think you need to give an actual value for highest on input or output since it is an internal temporary variable of the algorithm - it is sufficient that you can read and write it. This is expressed with data_at_. Then you can als remove h from the WITH clause.

view this post on Zulip Michael Soegtrop (Aug 03 2023 at 09:45):

This saves the user of the function to supply a value for h - you don't really want a user of the function to bother finding out what the value of h might be, since it is an internal detail of the function.

view this post on Zulip Paolo Giarrusso (Aug 03 2023 at 11:36):

in this program, h/highest is not internal to factorize, but only to find.

view this post on Zulip Paolo Giarrusso (Aug 03 2023 at 11:40):

but YMMV — if you only ask find to return an arbitrary number, then factorize can hide info about h. What to hide and what to show can be a genuine design question — we needn't resolve the debate here, but I want to at least mention there is an option

view this post on Zulip Notification Bot (Aug 07 2023 at 18:08):

Lessness has marked this topic as resolved.


Last updated: Jun 23 2024 at 03:02 UTC