Why3 Standard Library index



References

A mutable variable, or ``reference'' in ML terminology, is simply a record with a single mutable field contents.


Generic references

Creation, access, and assignment are provided as ref, prefix !, and infix :=, respectively.

module Ref

  type ref 'a = { mutable contents "model_trace:" : 'a }

  function (!) (x: ref 'a) : 'a = x.contents

  let ref (v: 'a) ensures { result = { contents = v } } = { contents = v }

  let (!) (r:ref 'a) ensures { result = !r } = r.contents

  let (:=) (r:ref 'a) (v:'a) ensures { !r = v } = r.contents <- v

end

Integer References

a few operations specific to integer references

module Refint

  use import int.Int
  use export Ref

  let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1
  let decr (r: ref int) ensures { !r = old !r - 1 } = r := !r - 1

  let (+=)   (r: ref int) (v: int) ensures { !r = old !r + v } = r := !r + v
  let (-=)   (r: ref int) (v: int) ensures { !r = old !r - v } = r := !r - v
  let ( *= ) (r: ref int) (v: int) ensures { !r = old !r * v } = r := !r * v

end

Generated by why3doc 0.87.2