RE: Contracts meeting
Dimitrios Vytiniotis
Guys, just a reminder that we have a skype call at 1:15 today.
Thanks!
d-
From: Nathan Collins
Sent: Friday, November 25, 2011 2:28 PM
To: Haskell Contracts Project
Cc: Koen Claessen; Dimitrios Vytiniotis; Simon Peyton-Jones
Subject: RE: Contracts meeting
Hi all,
I created a mailing list for the project. You should have received an invite. Please send future project related emails to the list.
“Haskell Contracts Project” haskellc...@googlegroups.com
I made the list publicly viewable, like the source code. If anyone prefers it private let me know and I’ll change it.
Simon, thanks for writing up our meeting!
-nathan
From: Simon Peyton-Jones
Sent: 25 November 2011 14:00
To: Koen Claessen; Nathan Collins; Dimitrios Vytiniotis; Simon Peyton-Jones
Subject: Contracts meeting
Future: 1.15pm our time Tuesdays starting 29 Nov
Situation now
· Have ‘min’ translation
· Usability improvements
o Real Haskell syntax; can feed to type checker
o Can typecheck the contracts too
· Main problem: often need an inductive lemma
Tramslation
Have removed the “f does not satisfy c” translation.
“I want to prove the contract” [e in c]+
“I want to use the contract” [e in c]-
Details in the draft document https://github.com/cpa/haskellcontracts/blob/master/paper.tex
Lemmas
https://docs.google.com/document/d/1YYG5lYkLfsUiRoIpsDDRtHaGjwST3reqD2qHsj51zFY/edit?hl=en&pli=1
data Lemma = QED
using :: a -> Lemma -> a
p `using` QED = p
Sound; but downside is that (to be sound) the lemma has to be run at runtime.
NB that it’s not enough to to prove that the lemma terminates: it might be given bad values!
eg
BAD `using` lemma_eq_reflexive (let n = Succ n in n)
This seems like a better solution than the one Nathan was thinking about.
But: does (lemma_eq_reflexive x) terminate here?
f x = x `using` lemma_eq_reflexive x
f :: x:OK -> { y | eq x y }
mutter mutter mutter
Koen’s masters student
Dan Rosen
· Haskell -> FOL
· Including nested patterns, guards
· Generating FOL formulae that embody a variety of induction schemes:
o induction over a set of variables
o approximation lemma
o fixpoint induction (this is more or less what we are doing)
o recursion induction
· Goes way beyond Zeno
Still todo
· Do Zeno examples for interest (but don’t be too ambitious!)
· Do Catch examples
· Arithmetic not a good test case
· Take some real programs and look for crash freeness
risers :: Ord α→[α] →[[α]]
risers [] = []
risers [x] = [[x]]
risers (x:y:etc)
= if x ≤y then (x:s) : ss else [x] : (s : ss)
where s:ss= risers (y : etc)
Can the pattern match on the last line fail to match?
Needs one unfolding! Serendipity
http://community.haskell.org/~ndm/catch/
· Koen will think how other inductions can be used for contract checking
Counter examples
function f
contract f ::: C
f has arity 3
when you generate formula, stating that f satisfies a contract, make sure arguments to f are called a_1 a_2 a_3
ie the last thing in the TPTP file is not( f satisfies C ), and it’s *this* formula that uses the skolem arguments a_1 etc.
Dimitrios Vytiniotis
Actually, can we make it just a tiny a bit later? 13:30? Thanks
d-
Nathan Collins
> From: Simon Peyton-Jones
> Sent: Friday, November 25, 2011 2:00 PM
> To: Koen Claessen; Nathan Collins; Dimitrios Vytiniotis; Simon Peyton-Jones
> risers :: Ord α→[α] →[[α]]
>
> risers [] = []
>
> risers [x] = [[x]]
>
> risers (x:y:etc)
>
> = if x ≤y then (x:s) : ss else [x] : (s : ss)
>
> where s:ss= risers (y : etc)
>
> Can the pattern match on the last line fail to match?
>
> Needs one unfolding! Serendipity
>
> http://community.haskell.org/~ndm/catch/
We got this example, and the 'x + S y = S (x + y)' example, working
[1]. Problem was that our contract for risers was too weak, and we
needed a lemma for the base case of the arithmetic example.
We did *not* need unfolding for 'risers'.
I'm CC'ing Simon and Dimitrios here, because MS is bouncing the their
messages sent from the google group :P
-nathan
[1] https://github.com/cpa/haskellcontracts-examples/commit/cff012189964d7c6640ee8444b1bbe792c2a1aa0
Nathan Collins
-- 1.
--
-- This is necessary because we need 'not . null -> not . null' to
-- have a usable inductive hypothesis.
{-# CONTRACT
risers ::: xs:(CF&&{xs: not (null xs)}) -> CF&&{xs: not (null xs)}
#-};;
-- 2.
--
-- This is unnecessary but provable.
-- {-# CONTRACT
-- risers ::: xs:(CF&&{xs: null xs}) -> CF
-- #-};;
-- 3.
--
-- This is not provable without the 'not (null x)' version. NB: no
-- unrollings are needed.
{-# CONTRACT
risers ::: xs:CF -> CF
#-};;
Using the '--only-check risers' option to avoid checking the 'le' and
'ge' lemmas (we checked them once), and on a machine with load
average > 13 (!!!), the time it takes to check 'risers' is:
(1) 30s
(1),(3) 90s
(1),(2),(3) 160s
(3) 18s (and returns satisfiable)
-nathan
2011/12/12 Nathan Collins <nathan....@gmail.com>: