Abstract Refinement Types.ppt

《Abstract Refinement Types.ppt》由会员分享，可在线阅读，更多相关《Abstract Refinement Types.ppt（105页珍藏版）》请在麦多课文档分享上搜索。

1、Abstract Refinement Types,Niki Vazou1, Patrick M. Rondon2, and Ranjit Jhala1 1UC San Diego 2Google,1,Vanilla Types,12 : Int,2,Refinement Types,12 : v: Int | v 10 ,3,Refinement Types,12 : v: Int | v = 12 ,4,Refinement Types,12 : v: Int | v = 12 ,v = 12 0 v 20 even v,5,Refinement Types,12 : : v: Int |

2、 v = 12 : v: Int | 0 v 20 even v ,v = 12 0 v 20 even v,6,Refinement Types,12 : : v: Int | v = 12 12 : : v: Int | 0 v 20 even v ,7,A max function,max : Int - Int - Intmax x y = if x y then x else y,8,A refined max function,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,9,Using max,

3、max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,b = max 8 12 - assert (b 0),max 8 12 : v : Int | v x v y 8/x12/y,10,Using max,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,max 8 12 : v : Int | v 8 v 12 ,11,b = max 8 12 - assert (b 0),Using max,max:x:Int - y:Int

4、- v:Int | v x v ymax x y = if x y then x else y,max 8 12 : v : Int | v 12 ,12,b = max 8 12 - assert (b 0),Using max,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,v 12 v 0,13,b = max 8 12 - assert (b 0),Using max,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,ma

5、x 8 12 : v : Int | v 0 ,14,b = max 8 12 - assert (b 0),b = max 8 12 - assert (b 0),Using max,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,max 8 12 : v : Int | v 0 ,15,Using max,max:x:Int - y:Int - v:Int | v x v ymax x y = if x y then x else y,We get max 3 5 : v : Int | v 5 ,We w

6、antmax 3 5 : v : Int | v 5 odd v ,16,b = max 8 12 - assert (b 0)c = max 3 5 - assert (odd c),Using max,Problem: Information of Input Refinements is Lost,We get max 3 5 : v : Int | v 5 ,17,We wantmax 3 5 : v : Int | v 5 odd v ,Problem: Information of Input Refinements is Lost,Solution: Parameterize T

7、ype Over Input Refinement,Our Solution,18,Abstract Refinements,Solution: Parameterize Type Over Input Refinement,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,19,Abstract Refinements,Solution: Parameterize Type Over Input Refinement,max:forall Prop. Int - Int - Intmax x y = if x y t

8、hen x else y,20,Abstract refinement,“if both arguments satisfy p, then the result satisfies p”,Abstract Refinements,Solution: Parameterize Type Over Input Refinement,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,21,Abstract refinement,“if both arguments satisfy p, then the result sa

9、tisfies p”,Abstract Refinements,Solution: Parameterize Type Over Input Refinement,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,22,Abstract refinement,“if both arguments satisfy p, then the result satisfies p”,Abstract Refinements,Solution: Parameterize Type Over Input Refinement,ma

10、x:forall Prop. Int - Int - Intmax x y = if x y then x else y,23,Abstract refinement,“if both arguments satisfy p, then the result satisfies p”,Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max : forall Prop. Int - Int - Int,24,b = max (0) 8 12 - assert (b 0)c = max odd 3 5

11、 - assert (odd c),Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max : forall Prop. Int - Int - Int,25,b = max (0) 8 12 - assert (b 0)c = max odd 3 5 - assert (odd c),Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max odd : Int - Int - Int odd/p,26

12、,Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max odd : v:Int | odd v - v:Int | odd v - v:Int | odd v ,27,Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,3 : v:Int | odd v ,max odd : v:Int | odd v - v:Int | odd v - v:Int | odd v ,28,Using max,max:

13、forall Prop. Int - Int - Intmax x y = if x y then x else y,max odd 3 : v:Int | odd v - v:Int | odd v ,3 : v:Int | odd v ,29,b = max (0) 8 12 - assert (b 0)c = max odd 3 5 - assert (odd c),Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max odd 3 : v:Int | odd v - v:Int | odd

14、 v ,5 : v:Int | odd v ,30,b = max (0) 8 12 - assert (b 0)c = max odd 3 5 - assert (odd c),Using max,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,max odd 3 5 : v:Int | odd v ,5 : v:Int | odd v ,31,b = max (0) 8 12 - assert (b 0)c = max odd 3 5 - assert (odd c),Using max,max:forall P

15、rop. Int - Int - Intmax x y = if x y then x else y,max odd 3 5 : v:Int | odd v ,32,b = max (0) 8 12 - assert (b 0)c = max odd 3 5 - assert (odd c),Abstract Refinements,Solution: Parameterize Type Over Input Refinement,max:forall Prop. Int - Int - Intmax x y = if x y then x else y,33,Abstract refinem

16、ent,“if both arguments satisfy p, then the result satisfies p”,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinements,34,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recurs

17、ive Refinements,35,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinements,36,A polymorphic max function,max : a - a - amax x y = if x y then x else y,We get max v:Int | odd v 3 5 : v:Int | odd v ,We instantiate a := v:Int | odd v

18、,37,c = max 3 5 - assert (odd c),Type Class Constraints,max : Ord a = a - a - amax x y = if x y then x else y,We get max v:Int | odd v 3 5 : v:Int | odd v ,We instantiate a := v:Int | odd v ,38,c = max 3 5 - assert (odd c),b = max 3 5 - assert (odd b)c = minus 3 5 - assert (odd c),Unsound Reasoning,

19、minus : Num a = a - a - aminus x y = x - y,We get minus v:Int | odd v 3 5 : v:Int | odd v ,We instantiate a := v:Int | odd v ,Abstract Refinements and Type Classes,max :forall Prop. Ord a = a - a - amax x y = if x y then x else y,We get max Int odd 3 5 : v:Int | odd v ,40,b = max Int odd 3 5- assert

20、 (odd b),Abstract Refinements and Type Classes,41,b = max Int odd 3 5 - assert (odd b)c = minus Int 3 5 - assert (odd b),minus : Num a = a - a - aminus x y = x - y,We get minus Int 3 5 : Int,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recurs

21、ive Refinements,42,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinements,43,A loop function,44,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,A loop function,loop

22、: (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,45,loop iteration,next acc,final result,A loop function,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,46,initial index,loop f

23、 n z = fn(z),initial acc,A loop function,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,loop f n z = fn(z),A loop function,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = ac

24、c,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,48,A loop function,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,49,incr acc by 1,A loop func

25、tion,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,50,incr acc by 1,Inductive Proof,R : (Int, a),51,Loop Invariant:,loop : (Int - a - a) - Int - a - aloop f n z = g

26、o 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,loop iteration,accumulator,Inductive Proof,R(0, z),R(i, acc) R(i+1, f i acc),R : (Int, a),52,Base:,Inductive Step:,Loop Invariant:,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwi

27、se = acc,R(n, loop f n z),Conclusion:,Induction via Abstract Refinements,53,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,z : a,Induction via Abstract Refinements,54,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i ac

28、c | i n = go (i+1) (f i acc)| otherwise = acc,R(0, z),R(i, acc) R(i+1, f i acc),R : (Int, a),R(n, loop f n z),r : Int - a - Prop,f : i:Int - a - a,Induction via Abstract Refinements,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,R(0,

29、z),R(i, acc) R(i+1, f i acc),R : (Int, a),R(n, loop f n z),r : Int - a - Prop,z : a,Induction via Abstract Refinements,56,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,R(0, z),R(i, acc) R(i+1, f i acc),R : (Int, a),R(n, loop f n z),r

30、 : Int - a - Prop,z : a,f : i:Int - a - a,loop f n z : a,0,Induction via Abstract Refinements,57,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,r : Int - a - Prop,z : a,f : i:Int - a - a,loop f n z : a,Induction via Abstract Refinemen

31、ts,loop : forall a - Prop.f:(i:Int - a - a) - n: v:Int | v=0 - z:a- a,58,loop : (Int - a - a) - Int - a - aloop f n z = go 0 z where go i acc | i n = go (i+1) (f i acc)| otherwise = acc,Induction via Abstract Refinements,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc)

32、acc = i + z,loop : forall a - Prop.f:(i:Int - a - a) - n: v:Int | v=0 - z:a- a,59,incr acc by 1,Induction via Abstract Refinements,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc) acc = i + z,loop i acc - acc = i + z: f:(i:Int - v:a | v=i+z - v:a | v=(i+1)+z) - n:v:Int

33、| v=0- z:Int- v:Int | v=n+z,60,Induction via Abstract Refinements,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc) acc = i + z,loop i acc - acc = i + z: f:(i:Int - v:a | v=i+z - v:a | v=(i+1)+z) - n:v:Int | v=0- z:Int- v:Int | v=n+z,61,Induction via Abstract Refinements

34、,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc) acc = i + z,loop i acc - acc = i + z f: n:v:Int | v=0- z:Int- v:Int | v=n+z,62,Induction via Abstract Refinements,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc) acc = i + z,loop i acc - ac

35、c = i + z f: n:v:Int | v=0- z:Int- v:Int | v=n+z,63,Induction via Abstract Refinements,incr : Int - Int - Int incr n z = loop f n z where f i acc = acc + 1,R(i, acc) acc = i + z,incr: n:v:Int | v=0- z:Int- v:Int | v=n+z,64,Induction via Abstract Refinements,incr : n:v:Int | v=0- z:Int- v:Int | v=n+z

36、incr n z = loop f n z where f i acc = acc + 1,65,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinements,66,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinement

37、s,67,A Vector Data Type,data Vec a = V f : i:Int - a,68,Goal: Encode the domain of Vector,Encoding the Domain of a Vector,data Vec Prop a = V f : i:Int - a,69,Abstract refinement,index satisfies d,Encoding the Domain of a Vector,70,data Vec Prop a = V f : i:Int - a,Encoding the Domain of a Vector,da

38、ta Vec Prop a = V f : i:Int - a,“vector defined on positive integers”,71,Vec v 0 a,Encoding the Domain of a Vector,data Vec Prop a = V f : i:Int - a,“vector defined only on 1”,72,Vec v = 1 a,Encoding the Domain of a Vector,data Vec Prop a = V f : i:Int - a,“vector defined on the range 0 n”,73,Vec 0

39、v a,data Vec Prop, r:Int - a - Prop a = V f : i:Int - a,Encoding Domain and Range of a Vector,74,Encoding Domain and Range of a Vector,75,data Vec Prop, r:Int - a - Prop a = V f : i:Int - a,Encoding Domain and Range of a Vector,“vector defined on positive integers, with values equal to their index”,

40、76,Vec v 0, i v - i = v Int,data Vec Prop, r:Int - a - Prop a = V f : i:Int - a,Encoding Domain and Range of a Vector,77,Vec v = 1, i v - v = 12 Int,“vector defined only on 1, with values equal to 12”,data Vec Prop, r:Int - a - Prop a = V f : i:Int - a,Null Terminating Strings,“vector defined on the

41、 range 0 n, with its last value equal to 0”,78,Vec 0 v i = n-1 = v = 0 Char,data Vec Prop, r:Int - a - Prop a = V f : i:Int - a,Fibonacci Memoization,“vector defined on positives, with i-th value equal to zero or i-th fibonacci”,79,Vec 0 v, i v - v != 0 = v = fib(i) Int,data Vec Prop, r:Int - a - Pr

42、op a = V f : i:Int - a,Using Vectors,80,Abstract over d and r in vector op (get, set, )Specify vector properties (NullTerm, FibV, )Verify that user functions preserve properties,81,Using Vectors,type NullTerm n = Vec 0 i=n-1 = v=0 Char upperCase : n:v: Int| v0 - NullTerm n - NullTerm n upperCase n s

43、 = ucs 0 s where ucs i s = case get i s of 0 - s c - ucs (i + 1) (set i (toUpper c) s),Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,Indexed Refinements,Recursive Refinements,82,Outline,Evaluation,Applications,Refinements and Type Classes,Inductive Refinements,In

44、dexed Refinements,Recursive Refinements,83,List Data Type,Goal: Relate tail elements with the head,data List a= N| C (h : a) (tl : List a),84,data List a a - Prop= N| C (h : a) (tl : List (a),Recursive Refinements,85,Abstract refinement,tail elements satisfy p at h,Unfolding Recursive Refinements,86

45、,data List a a - Prop= N| C (h : a) (tl : List (a),Unfolding Recursive Refinements,87,h1 C h2 C h3 C N : List a,data List a a - Prop= N| C (h : a) (tl : List (a),Unfolding Recursive Refinements (1/3),88,h1 C h2 C h3 C N : List a,h1 : a tl1 : List (a),data List a a - Prop= N| C (h : a) (tl : List (a)

46、,Unfolding Recursive Refinements (2/3),89,h1 C h2 C h3 C N : List a,h1 : a h2 : a tl2 : List (a),data List a a - Prop= N| C (h : a) (tl : List (a),Unfolding Recursive Refinements (3/3),h1 C h2 C h3 C N : List a,h1 : a h2 : a h3 : a N : List (a),90,data List a a - Prop= N| C (h : a) (tl : List (a),In

47、creasing Lists,91,h1 C h2 C h3 C N : IncrL a,data List a a - Prop= N| C (h : a) (tl : List (a),type IncrL a = List hd v a,Increasing Lists,h1 C h2 C h3 C N : IncrL a,h1 : a h2 : v:a | h1 v h3 : v:a | h1 v h2 v N : IncrL v:a | h1 v h2 v h3 v ,92,type IncrL a = List hd v a,data List a a - Prop= N| C (h : a) (tl : List (a),