Question : inv_proof

[alanz]

I see tutorial 12 needs inv_proof

{-@ invariant {v:AVL a | 0 <= realHeight v && realHeight v = getHeight v} @-}

{-@ inv_proof  :: t:AVL a -> {v:_ | 0 <= realHeight t && realHeight t = getHeight t } @-}
inv_proof Leaf           = True
inv_proof (Node k l r n) = inv_proof l && inv_proof r

This is another thing that is not introduced earlier.

I think some sort of glossary of accepted liquid haskell annotations and their interpretation would be a good thing. Perhaps split into core and experimental/deprecated.

[ranjitjhala]

Good catch!

This is a mechanism is now redundant and can be deprecated; I will update this chapter to remove it. (Instead one can just put the relevant facts into the output types of the measures.)

Right @nikivazou?

On Wed, Mar 15, 2017 at 2:41 PM Alan Zimmerman notifications@github.com wrote:

I see tutorial 12 needs inv_proof

{-@ invariant {v:AVL a | 0 <= realHeight v && realHeight v = getHeight v} @-}

{-@ invproof :: t:AVL a -> {v: | 0 <= realHeight t && realHeight t = getHeight t } @-} inv_proof Leaf = True inv_proof (Node k l r n) = inv_proof l && inv_proof r

This is another thing that is not introduced earlier.

I think some sort of glossary of accepted liquid haskell annotations and their interpretation would be a good thing. Perhaps split into core and experimental/deprecated.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/956, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOBZ7wn0wHMf37pPebyNYVrl69s56ks5rl6tbgaJpZM4MdqsE .

[alanz]

Something else: It was SAFE, I commented out those lines, and it still came out SAFE. But after blowing away the ..liquid directory it failed again, as expected.

[ranjitjhala]

Ah, thats because of the (still somewhat buggy) "diff check" mode at the top of the file in

{-@ LIQUID "--diff" @-}

Thanks to recent improvements, most of these files are fast enough without this, so I'll just disable it on the entire tutorial!

On Wed, Mar 15, 2017 at 4:39 PM, Alan Zimmerman notifications@github.com wrote:

Something else: It was SAFE, I commented out those lines, and it still came out SAFE. But after blowing away the ..liquid directory it failed again, as expected.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/956#issuecomment-286711003, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOOrqRjqp1tK8FsCJ-BViVPzjupdMks5rl8bwgaJpZM4MdqsE .

[nikivazou]

Correct, you can replace the invariant with proper refinements in the result types of realHeight getHeight