Static Contract Checking for Haskell

0 comments

file time: 2008-02-16

filetype:ppt

Click Here To Download...

>  

1  

Static Contract Checking for Haskell 

Dana N. Xu

University of Cambridge

Joint work with  
 

Simon Peyton Jones

Microsoft Research Cambridge 

Koen Claessen

Chalmers University of Technology

 

2  

Module UserPgm where 

f :: [Int]->Int

f xs = head xs `max` 0  

    :

    00f [] 00/b> 

Program Errors Give Headache! 

Glasgow Haskell Compiler (GHC) gives at run-time 

      Exception: Prelude.head: empty list 

Module Prelude where 

head :: [a] -> a

head (x:xs) = x

head [] = error 00mpty list00/b>

 

3  

Types>> > > > > Contracts >> > > > >  

head (x:xs) = x 

head :: [Int] -> Int 

00/b>(head 1)00/b> 
 

head 2 {xs | not (null xs)} -> {r | True} 
 

00/b>(head [])00/b> 

Bug! 

Bug! 

Contract

(original Haskell boolean expression) 

Type 

not :: Bool -> Bool

not True = False

not False = True 

null :: [a] -> Bool

null [] = True

null (x:xs) = False

 

4  

Contract Checking 

head 2 {xs | not (null xs)} -> {r | True}

head (x:xs00 = x 

f xs = head xs `max` 0 

Warning: f [] calls head

         which may fail head00 precondition! 

f_ok xs = if null xs then 0

          else head xs `max` 0 

No more warnings from compiler!

 

5  

Satisfying a predicate contract 

e 2 {x | p}  if   (1)   p[e/x] gives True  and

                        (2)  e is crash-free. 

Arbitrary boolean-valued Haskell expression 

Recursive function,

higher-order function, partial function

can be called!

 

6  

Expressiveness of  
the Specification Language 

data T = T1 Bool | T2 Int | T3 T T 

sumT :: T -> Int

sumT 2 {x | noT1 x} -> {r | True}

sumT (T2 a) = a

sumT (T3 t1 t2) = sumT t1 + sumT t2 

noT1 :: T -> Bool

noT1 (T1 _) = False

noT1 (T2 _) = True

noT1 (T3 t1 t2) = noT1 t1 && noT1 t2

 

7  

Expressiveness of  
the Specification Language 

sumT :: T -> Int

sumT 2 {x | noT1 x} -> {r | True}

sumT (T2 a) = a

sumT (T3 t1 t2) = sumT t1 + sumT t2 

rmT1 :: T -> T

rmT1 2 {x | True} -> {r | noT1 r}

rmT1 (T1 a) = if a then T2 1 else T2 0

rmT1 (T2 a) = T2 a

rmT1 (T3 t1 t2) = T3 (rmT1 t1) (rmT1 t2) 

For all crash-free t::T,   sumT (rmT1 t) will not crash.

 

8  

Higher Order Functions 

all :: (a -> Bool) -> [a] -> Bool

all f [] = True

all f (x:xs) = f x && all f xs 

filter :: (a -> Bool) -> [a] -> [a]

filter 2 {f | True} -> {xs | True} -> {r | all f r}

filter f [] = []

filter f (x:xs00 = case (f x) of

                   True -> x : filter f xs00/b>

                   False -> filter f xs00/b>

 

9  

Contracts for higher-order function00 parameter 

f1 :: (Int -> Int) -> Int

f1 2 ({x | True} -> {y | y >= 0}) -> {r | r >= 0}

f1 g = (g 1) - 1 

f2:: {r | True}

f2 = f1 (\x -> x 001) 

Error: f100 postcondition fails

       because (g 1) >= 0 does not imply

               (g 1) 001 >= 0

Error: f2 calls f1

       which fails f100 precondition 

[Findler&Felleisen:ICFP002, Blume&McAllester:ICFP004]

 

10  

Functions without Contracts 

data T = T1 Bool | T2 Int | T3 T T 

noT1 :: T -> Bool

noT1 (T1 _) = False

noT1 (T2 _) = True

noT1 (T3 t1 t2) = noT1 t1 && noT1 t2 

(&&) True x = x

(&&) False x = False 

No abstraction is more compact than

the function definition itself!

 

11  

Contract Synonym 

contract Ok = {x | True}

contract NonNull = {x | not (null x)} 

head :: [Int] -> Int

head 2 NonNull -> Ok

head (x:xs) = x 

{-# contract Ok = {x | True} -#}

{-# contract NonNull = {x | not (null x)} #-}

{-# contract head :: NonNull -> Ok #-} 

Actual Syntax

 

12  

Questions on e 2 t 

bot = bot 

00x. x                2  {x | bot} ! {r | True} ? 

00x. error 0000nbsp;  2  {x | bot} ! {r | True}  ?

00x. x                 2  {x | True} ! {r | bot}  ?

00x. head []       2  {x | True} ! {r | bot}  ?

(True, 2)          2  {x | (snd x) > 0}     ?

(head [], 3)      2   {x | (snd x) > 0}     ?

error 0000nbsp;        2   ?

    ?                   2  {x | False}

    ?                   2  {x | head []}        

 

13  

Language 
Syntax 

following Haskell00

lazy semantics

 

14  

Two special constructors 

BAD is an expression that crashes.

error :: String -> a

error s = BAD 

head (x:xs) = x

head [] = BAD 

UNR (short for 00nreachable00 is an expression that gets stuck. This is not a crash, although execution comes to a halt without delivering a result. (identifiable infinite loop)  

15  

Syntax of Contracts 
(related to [Findler:ICFP02,Blume:ICFP04,Hinze:FLOPS06,Flanagan:POPL06])  

Full version:  x00{x | x >0} -> {r | r > x00

Short hand:  {x | x > 0} -> {r | r > x} 

k:({x | x > 0} -> {y | y > 0}) -> {r | r > k 5} 

t 2 Contract

t ::= {x | p}    Predicate Contract

   |  x:t1 ! t2  Dependent Function Contract

   |  (t1, t2)    Tuple Contract

   |  Any        Polymorphic Any Contract

 

16  

Contract Satisfaction 
(related to [Findler:ICFP02,Blume:ICFP04,Hinze:FLOPS06]) 

e" means e diverges or e !* UNR 

e 2 {x | p}      ,    e" or (e is crash-free and                                      p[e/x]!*{BAD, False}           [A1] 

e2 x:t1! t2    ,    e" or  8 e1 2 t1. (e e1) 2 t2[e1/x]        [A2] 

e 2 (t1, t2)       ,    e" or (e1 2 t1 and e2 2 t2)                 [A3] 

e 2 Any    ,    True                                                  [A4] 

Given ` e :: 00/b> and `c t :: 00/b>, we define e 2 t as follows:

 

17  

Answers on e 2 t 

00x. x         2  {x | bot} ! {r | True}  

00x. BAD   2  {x | bot} ! {r | True}  

00x. x         2  {x | True} ! {r | bot} 

00x. BAD   2  {x | True} ! {r | bot}  

00x. BAD   2  {x | True} ! Any

(True, 2)    2  {x | (snd x) > 0}    

(BAD, 3)   2   {x | (snd x) > 0}    

BAD          2   Any

UNR, bot   2  {x | False}

UNR, bot   2  {x | BAD}        

BAD 2 (Any, Any)  BAD 2 Any ! Any

 

18  

Lattice for Contracts  

{x | True} 

Any 

{x | False} 

({x | x>0}, Any) 

({x | x>0},

{r | r>0}) 

{x | x>0}->{r | r>x} 

Any -> {r | r>0}

 

19  

Laziness 
 

fst 2 ({x | True}, Any) -> {r | True}

fst (a,b) = a

00/b>fst (5, error 00/b>f00/b>)00/b> 

fstN :: (Int, Int) -> Int

fstN 2 ({x | True}, Any) -> {r | True}

fstN (a, b) n = if n > 0

                then fstN (a+1, b) (n-1)

                      else a 

g2 = fstN (5, error 00stN00 100 

Every expression satisfies Any

 

20  

What to Check? 

Does function f satisfies its contract t (written f2 t)? 

At the definition of each function f,

Check f 2 t assuming all functions called in f satisfy their contracts. 

Goal: main 2 {x | True}

 

21  

How to Check? 

Define

e 2 t 

Construct

e B t

(e 00/b>ensures00/b> t) 

Grand Theorem

e 2 t    ,    e B t is crash-free   

(related to Blume&McAllester:ICFP004) 

Normal form e00/b> 

Simplify (e B t) 

If e00/b> is syntactically safe,

then Done! 

This Talk 

ESC/Haskell (Xu:HW006)

 

22  

What we can00 do? 

g1, g2 2 Ok -> Ok

g1 x = case (prime x > square x) of

          True -> x

          False -> error 00rk00/b> 

g2 xs ys =

  case (rev (xs ++ ys) == rev ys ++ rev xs) of

    True -> xs

    False -> error 00rk00/b> 
 

Hence, three possible outcomes:

    (1) Definitely Safe (no crash, but may loop)

    (2) Definite Bug (definitely crashes)

    (3) Possible Bug 

Crash! 

Crash!

 

23  

Crashing 

Definition (Crash).

A closed term e crashes iff e !* BAD 

Definition (Crash-free Expression)

An expression e is crash-free iff

8 C. BAD 2 C, ` C[[e]] :: (), C[[e]]  !* BAD

 

24  

Definition of B and  C  
(B pronounced ensures  C pronounced requires) 

e B {x | p}

= case p[e/x] of

         True -> e

         False -> BAD 

e C {x | p}

= case p[e/x] of  True -> e

         False -> UNR 

Example:

5 2 {x | x > 0}

5 B {x | x > 0}

= case (5 > 0) of

     True -> 5

     False -> BAD 
 

related to [Findler:ICFP02,Blume:ICFP04,Hinze:FLOPS06]

 

25  

e B  x:t1 ! t2 

= 00/b> v. (e (vC t1)) B t2[vCt1/x] 

e C  x:t1 ! t2

= 00/b> v. (e (vB t1)) C t2[vBt1/x] 

e B (t1, t2)

= case e of

   (e1, e2) -> (e1 B t1, e2 B t2) 

e C  (t1, t2)

= case e of

   (e1, e2) -> (e1 C t1, e2 C t2) 

Definition of B and  C (cont.)

 

26  

Higher-Order Function 

f1 B ({x | True} -> {y | y >= 0}) -> {r | r >= 0}

= 00/b>      B                        C                B

= 00/b> v1. case (v1 1) >= 0 of

        True -> case (v1 1) - 1 >= 0 of

                True -> (v1 1) -1

                False -> BAD

        False -> UNR   

f1 :: (Int -> Int) -> Int

f1 2 ({x | True} -> {y | y >= 0}) -> {r | r >= 0}

f1 g = (g 1) - 1 

f2:: {r | True}

f2 = f1 (\x -> x 001)

 

27  

Modified Definition of B and  C  

e B {x | p}

= case p[e/x] of

         True -> e

         False -> BAD 

e B {x | p}

= e `seq` case fin (p[e/x]) of

               True -> e

               False -> BAD 

old 

new 

e_1 `seq` e_2 = case e_1 of {DEFAULT -> e_2} 

if e !* BAD,

then (fin e) ! False

else (fin e) ! e

 

28  

Why need seq and fin? 

    (UNR B {x | False}) !* BAD

But  UNR 2 {x | False}

         00x. x 2 {x | BAD} ! {x | True}

But 00/b> x. x B {x | BAD} ! {x | True}

!* 00/b> v. (v `seq` BAD) which is NOT crash-free. 

e B {x | p}

= e `seq` case fin (p[e/x]) of

               True -> e

               False -> BAD 

Without seq 

Without fin

 

29  

e B Any = UNR

e C Any = BAD 

f5 2 Any -> {r | True}

f5 x = 5 

error :: String -> a         -- HM Type

error 2 {x | True} -> Any  -- Contract 

Definition of B and  C for Any

 

30  

Properties of B and C 

Key Lemma:

For all closed, crash-free e, and closed t,

(e C t) 2 t 

Projections:  (related to Findler&Blume:FLOPS006)

For all e and t, if e 2 t, then

e 鹿 e B t e C t 鹿  e  

Definition (Crashes-More-Often):

e1 鹿  e2  iff   for all C, ` C[[ei]] :: () for i=1,2 and

                    C[[e2]] !* BAD ) C[[e1]] !* BAD

 

31  

About 30 Lemmas 00/b> 

Lemma [Monotonicity of Satisfaction ]:

If e1 2 t and e1 鹿 e2, then e22 t

Lemma [Congruence of 鹿]:

e1 鹿 e2     )    8 C. C[[e1]] 鹿 C[[e2]]

Lemma [Idempotence of Projection]:

8 e, t.   e B t B t 00e B t

8 e, t.   e C t C t 00eC t

Lemma [A Projection Pair]:

8 e, t.  e B t C t 鹿 e

Lemma [A Closure Pair]:

8 e, t.  e 鹿 eC t B t

 

32  

Lattice for Expressions (鹿 ) 

UNR 

BAD 

(3,BAD) 

5 

00x . x 

(3, 4) 

00x. 6

 

33  

Lattice for Contracts  

{x | True} 

Any 

{x | False} 

({x | x>0}, Any) 

({x | x>0},

{r | r>0}) 

{x | x>0}->{r | r>x} 

Any -> {r | r>0}

 

34  

Conclusion 

Contract 

Haskell Program 

Glasgow Haskell Compiler (GHC) 

Where the bug is 

Why it is a bug

 

35  

Contributions 

Automatic static contract checking instead of dynamic contract checking. Compared with ESC/Haskell Allow pre/post specification for higher-order function00 parameter through contracts. Reduce more false alarms caused by Laziness and in an efficient way. Allow user-defined data constructors to be used to define contracts Specifications are more type-like, so we can define contract synonym. We develop a concise notation (B and C) for contract checking, which enjoys many properties. We give a new and relatively simpler proof of the soundness and completeness of dynamic contract checking, this proof is much trickier than it looks. We implement the idea in GHC Accept full Haskell Support separate compilation as the verification is modular. Can check functions without contract through CEG unrolling.  

36  

Sorting 

sorted [] = True

sorted (x:[]) = True

sorted (x:y:xs) = x <= y && sorted (y : xs) 

insert :: {i | True} -> {xs | sorted xs}

       -> {r | sorted r} 

merge :: [Int] -> [Int] -> [Int]

merge :: {xs | sorted xs} -> {ys | sorted ys}

      -> {r | sorted r} 

bubbleHelper :: [Int] -> ([Int], Bool)

bubbleHelper :: {xs | True}

             -> {r | not (snd r) ==> sorted (fst r)}  

Insertsort, mergesort, bubblesort :: {xs | True}

                                  -> {r | sorted r} 

(==>) True x = x

(==>) False x = True

 

37  

Various Examples 

zip :: [a] -> [b] -> [(a,b)]

zip :: {xs | True} -> {ys | sameLen xs ys}

    -> {rs | sameLen rs xs } 

sameLen [] [] = True

sameLen (x:xs) (y:ys) = sameLen xs ys

sameLen _ _ = False  
 

f91 :: Int -> Int

f91 :: { n <= 101 } -> {r | r == 91 }

f91 n = case (n <= 100) of

           True -> f91 (f91 (n + 11))

          False -> n 0010

 

38  

f :: {x | x > 0} -> {r | True}

f x = x 

f B {x | x > 0} -> {r | True}

=(00/b>x.x) B {x | x > 0} -> {r | True}

= 00/b>v. (00/b>x.x (v C {x | x > 0})) B {r | True}

= 00/b>v. (case v > 0 of

         True -> v

         False -> UNR) 

g = 00 f00/b> 

f C {x | x > 0} -> {r | True}

= 00/b>v. (case v > 0 of

         True -> v

         False -> BAD)

 

39  

Constructor Contracts 

{x | x > 0} : {xs | all (< 0) xs}

{x | x > 0} : Any

Any : Any 

Support any user-defined data constructors!

(related to [Hinze&Jeuring&L枚h:FLOPS006])

 

40  

How to Check e 2 t? 

Given e and t

We construct a term (eBt) (pronounced e 00/font>ensures00/font> t) related to Findler&Felleisen:ICFP002 (dynamic contract checking algorithm) Prove (eBt) is crash-free. simplify the term (eBt) to e00and e00is syntactically safe, then we are done.  

Theorem 1       (related to Blume&McAllester:ICFP004)

eBt is crash-free  ,  e 2 t 

Theorem 2

simpl (eBt) is syntactically safe ) eBt is crash-free  

This Talk 

ESC/Haskell (HW006)

 

41

 

42

 

citations

 

43

 

44

 

52

 

46

 

45

 

51

 

Crash-free regardless of any context it is placed.

 

48

 

47

 

53

   download Static Contract Checking for Haskell