-- File: bag2 -- This file treats implementation 2 of the example of bags. It follows the -- structure of Section 6.5.2, and is hence divided in the following parts. -- 1. Interface -- 2. Specification -- 3. Implementation -- 4c. Using a weaker specification -- 4d. Subset algebras 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, 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 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 Rep2 := List Nat Def ops2 := {empty = nil Nat, add = insert, card = count, bound = last O} : BagI Rep2 Def imp2 := pack BagI Rep2 ops2 : 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 IsInvarBagI := \Rep:*s.\Inv:Rep->*p.\ops:BagI Rep. Inv (ops`empty) /\ @m:Nat. @r:Rep. Inv r -> Inv (ops`add m r) Prove IsInvar_Ordered_ops2 : IsInvarBagI Rep2 Ordered ops2 Def Spec := \Rep:*s. \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->*p) -> BagI Rep -> *p Def ImplemSpec := \Rep:*s. \ops:BagI Rep. ExQ Inv : Rep->*p. Spec Rep Inv ops /\ IsInvarBagI Rep Inv ops Prove Spec_True__NaiveSpec : @R:*s.@opsR:BagI R. Spec R (\r:R. True) opsR -> NaiveSpec R opsR Prove NaiveSpec__Spec_True : @Rep:*s. @ops:BagI Rep. NaiveSpec Rep ops -> Spec Rep (\r:Rep. True) ops Def WeakUserSpec := \bagImp : BagImp. ExK Rep:*s. Ex ops:BagI Rep. ExQ Inv : Rep->*p. bagImp = pack BagI Rep ops /\ Spec Rep Inv ops /\ IsInvarBagI Rep Inv ops Prove Spec_Ordered_ops2 : Spec Rep2 Ordered ops2 Prove ImplemSpec_ops2 : ImplemSpec Rep2 ops2 Prove Implem__WeakUserSpec : @Rep:*s. @ops:BagI Rep. ImplemSpec Rep ops -> WeakUserSpec (pack BagI Rep ops) Prove WeakUserSpec_imp2 : WeakUserSpec imp2 ----------------------------------------- -- -- -- 4d. S U B S E T A L G E B R A S -- -- -- ----------------------------------------- Def IsSubsetAlg :=\R:*s. \opsR : BagI R. \Inv:R->*p. \S:*s. \opsS : BagI S. Ex inj:S->R. IsInjection inj /\ (Inv <==> Image inj) /\ SimBagI R S (\r:R.\s:S. r = inj s) opsR opsS : @R:*s. BagI R -> (R->*p) -> @S:*s. BagI S -> *p Var exis_SubsetAlg : @R:*s. @opsR:BagI R. @Inv:R->*p. IsInvarBagI R Inv opsR -> ExK S:*s. Ex opsS: BagI S. IsSubsetAlg R opsR Inv S opsS -- (i) prove pack_Subset : @R:*s. @opsR:BagI R. @Inv:R->*p. @S:*s. @opsS: BagI S. IsSubsetAlg R opsR Inv S opsS -> (=) BagImp (pack BagI R opsR) (pack BagI S opsS) -- (ii) Prove Spec_Sens : @R:*s. @opsR:BagI R. @Inv:R->*p. @S:*s. @opsS: BagI S. IsSubsetAlg R opsR Inv S opsS -> Spec R Inv opsR -> Spec S (\s:S. True) opsS Prove Implem__UserSpec : @Rep:*s. @ops:BagI Rep. ImplemSpec Rep ops -> UserSpec (pack BagI Rep ops) Prove UserSpec_imp2 : UserSpec imp2 Prove principle : @imp:BagImp. UserSpec imp -> @A:*s.@Q:A->*p.@body:@X:*s. BagI X -> A. (@X:*s.@ops:BagI X. Spec X (\r:X.True) ops -> Q (body X ops)) -> Q (unpack imp (\X:*s.\ops:BagI X. body X ops))