Mentions légales du service

Skip to content
Snippets Groups Projects
Open Forall construction in code for ghost binding
  • View options
  • Forall construction in code for ghost binding

  • View options
  • Open Issue created by François Bobot

    Sometimes when we want to prove such functions:

    let f x : result
      ensures { forall y. P(x,y) -> Q(x,y) }

    We need to prove with a ghost variable, for easing the proof

    let f' x (ghost y) : result
      requires { P(x,y) }
      ensures { Q(x,y) }

    However it is not possible to prove the first function using the second. We propose to add a new construction which allows it.

    let f x : result
      ensures { forall y. P(x,y) -> Q(x,y) }
     =
     forall y requires { P(x,y) } in 
      f' x y

    The semantic of this function is not completely clear:

    • should a VC be generated to check that it exists such y
    • what if the result contains a ghost
    • what if there are ghost effect
    • Merge request
    • Branch

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading