-- File: bag3 -- This file treats implementation 3 of the example of bags. It follows the -- structure of Section 6.5.3, and is hence divided in the following parts. -- 1. Interface -- 2. Specification -- 3. Implementation -- 4c. Using a weaker specification -- 4d. Combing quotients and subsets Path "../lol" Path "../lolExtra" Load "lambdaLplus" Load "list2" Load "prelims" ---------------------------- -- -- -- 1. I N T E R F A C E -- -- -- ---------------------------- Def BagI := \X:*s. {| empty : X, add : Nat -> X -> X, card : Nat -> X -> Nat, bound : X -> Nat |} Def BagImp := Sig X:*s. BagI X -- We introduce Sim, Bisim, IsInvar, and the parametricity axiom just for BagI; -- the general scheme cannot be formalized in Yarrow (see the discussion -- at the end of Section 6.7.6, on pages 190,191). Def SimBagI := \Rep1,Rep2:*s. \(~):Rep1 ->Rep2->*p. \ops1:BagI Rep1. \ops2:BagI Rep2. ops1`empty ~ ops2`empty /\ (@x:Rep1.@y:Rep2. @m:Nat. x ~ y -> ops1`add m x ~ ops2`add m y) /\ (@x:Rep1.@y:Rep2. @m:Nat. x ~ y -> ops1`card m x = ops2`card m y) /\ (@x:Rep1.@y:Rep2. x ~ y -> ops1`bound x = ops2`bound y) : @Rep1,Rep2:*s. (Rep1->Rep2->*p) -> BagI Rep1 -> BagI Rep2 -> *p Def BisimBagI := \Bag:*s.\(~): Bag->Bag->*p.\ops:BagI Bag. SimBagI Bag Bag (~) ops ops : @Bag:*s. (Bag->Bag->*p) -> BagI Bag -> *p Def IsInvarBagI := \Rep:*s.\Inv:Rep->*p.\ops:BagI Rep. Inv (ops`empty) /\ @m:Nat. @r:Rep. Inv r -> Inv (ops`add m r) Var parSigmaBagI : @X1:*s.@X2:*s.@x1:BagI X1. @x2:BagI X2. @(~) : X1->X2->*p. SimBagI X1 X2 (~) x1 x2 -> pack BagI X1 x1 = pack BagI X2 x2 ------------------------------------ -- -- -- 2. S P E C I F I C A T I O N -- -- -- ------------------------------------ Def NaiveSpec := \Bag:*s. \ops:BagI Bag. @m,n:Nat. @b:Bag. ops`card m ops`empty = O /\ ops`card m (ops`add m b) = S (ops`card m b) /\ (Not (m=n) -> ops`card m (ops`add n b) = ops`card m b) /\ ops`add m (ops`add n b) = ops`add n (ops`add m b) /\ (S O <= ops`card m b -> m <= ops`bound b) : @Bag:*s. BagI Bag -> *p Def UserSpec := \imp:BagImp. ExK Rep:*s. Ex ops:BagI Rep. imp = pack BagI Rep ops /\ NaiveSpec Rep ops -------------------------------------- -- -- -- 3. I M P L E M E N T A T I O N -- -- -- -------------------------------------- Def Rep3 := {| els : List Nat, mx : Nat |} Def ops3 := {empty = {els = nil Nat, mx=O}, add = \n:Nat. \r:Rep3. {els= n;r`els, mx= max r`mx n}, card = \n:Nat. \r:Rep3. count n r`els, bound = \r:Rep3. r`mx} : BagI Rep3 Def imp3 := pack BagI Rep3 ops3 : BagImp ------------------------------------------------------------------- -- -- -- 4c. U S I N G A W E A K E R S P E C I F I C A T I O N -- -- -- ------------------------------------------------------------------- Def Spec := \Rep:*s. \(~~) : Rep->Rep->*p. \Inv:Rep->*p. \ops:BagI Rep. @m,n:Nat. @r:Rep. Inv r -> ops`card m ops`empty = O /\ ops`card m (ops`add m r) = S (ops`card m r) /\ (Not (m=n) -> ops`card m (ops`add n r) = ops`card m r) /\ ops`add m (ops`add n r) ~~ ops`add n (ops`add m r) /\ (S O <= ops`card m r -> m <= ops`bound r) : @Rep:*s. (Rep->Rep->*p) -> (Rep->*p) -> BagI Rep -> *p Prove Spec_True__NaiveSpec : @R:*s.@opsR:BagI R. Spec R ((=) R) (\r:R. True) opsR -> NaiveSpec R opsR Prove NaiveSpec__Spec_True : @R:*s. @opsR:BagI R. NaiveSpec R opsR -> Spec R ((=) R) (\r:R. True) opsR Def ImplemSpec := \Rep:*s. \ops:BagI Rep. ExR (~~) : Rep->Rep->*p. ExQ Inv:Rep->*p. Spec Rep (~~) Inv ops /\ BisimBagI Rep (~~) ops /\ IsInvarBagI Rep Inv ops /\ IsERon (~~) Inv Def WeakUserSpec := \bagImp : BagImp. ExK Rep:*s. Ex ops:BagI Rep. ExR (~~) : Rep->Rep->*p. ExQ Inv : Rep->*p. bagImp = pack BagI Rep ops /\ Spec Rep (~~) Inv ops /\ BisimBagI Rep (~~) ops /\ IsERon (~~) Inv /\ IsInvarBagI Rep Inv ops Def Inv3 := \r:Rep3. @n:Nat. Elem n r`els -> n<=r`mx Prove IsInvar_Inv3 : IsInvarBagI Rep3 Inv3 ops3 Def Sim3 := \r,r':Rep3. Perm r`els r'`els /\ r`mx = r'`mx Prove Bisim_Sim3 : BisimBagI Rep3 Sim3 ops3 Prove IsERon_Sim3 : IsERon Sim3 Inv3 Prove Spec_ops3 : Spec Rep3 Sim3 Inv3 ops3 Prove ImplemSpec_ops3 : ImplemSpec Rep3 ops3 Prove WeakUserSpec_imp3 : WeakUserSpec imp3 ------------------------------------------------------------------------- -- -- -- 4d. C O M B I N I N G Q U O T I E N T S A N D S U B S E T S -- -- -- ------------------------------------------------------------------------- Def IsQuotSubsetAlg := \R:*s. \opsR : BagI R. \(~~) : R->R->*p. \Inv:R->*p. \Q:*s. \opsQ : BagI Q. ExR Rel:R->Q->*p. (Inv <==> Dom Rel) /\ (@q:Q. Ex r:R. Rel r q) /\ (@r,r':R. @q,q':Q. Rel r q -> Rel r' q' -> r~~r' <=> q=q') /\ SimBagI R Q Rel opsR opsQ : @R:*s. BagI R -> (R->R->*p) -> (R->*p) -> @Q:*s. BagI Q -> *p Var exis_QuotSubsetAlg : @R:*s. @opsR:BagI R. @(~~):R->R->*p. @Inv:R->*p. IsERon (~~) Inv -> BisimBagI R (~~) opsR -> IsInvarBagI R Inv opsR -> ExK Q:*s. Ex opsQ: BagI Q. IsQuotSubsetAlg R opsR (~~) Inv Q opsQ Prove pack_QuotSubset : @R:*s. @opsR:BagI R. @(~~):R->R->*p.@Inv:R->*p. @Q:*s. @opsQ:BagI Q. IsQuotSubsetAlg R opsR (~~) Inv Q opsQ -> pack BagI R opsR = pack BagI Q opsQ Prove Spec_Sens : @R:*s. @opsR:BagI R. @(~~):R->R->*p. @Inv:R->*p. @Q:*s. @opsQ: BagI Q. IsQuotSubsetAlg R opsR (~~) Inv Q opsQ -> Spec R (~~) Inv opsR -> Spec Q ((=) Q) (\q:Q.True) opsQ Prove Implem__UserSpec : @Rep:*s. @ops:BagI Rep. ImplemSpec Rep ops -> UserSpec (pack BagI Rep ops) Prove UserSpec_imp3 : UserSpec imp3 Prove principle : @imp:BagImp. UserSpec imp -> @A:*s.@Q:A->*p.@body:@X:*s. BagI X -> A. (@X:*s.@ops:BagI X. Spec X ((=) X) (\r:X.True) ops -> Q (body X ops)) -> Q (unpack imp (\X:*s.\ops:BagI X. body X ops))