An Electronic Purse: Specification, Refinement and Proof
Susan Stepney, David F. Cooper, Jim Woodcock · Kent Academic Repository (University of Kent) · 2000
StartTo 125 17.1 Proof obligation 125 17.2 Instantiating lemma 'deterministic' 126 17.3 Behaviour of maybeLost and definitelyLost 126 17.4 exists-pd 127 17.5 exists-chosenLost 127 17.6 check-operation 128 18 Req 129 18.1 Proof obligation 129 18.2 Instantiating lemma 'deterministic' 129 18.3 Discussion 130 18.4 exists-pd 131 18.5 exists-chosenlost 131 18.6 check-operation 131 18.7 case 1: ReqOkay and RabOkayClPd ′ 133 18.8 case 2: ReqOkay and RabWillBeLostPd ′ 138 18.9 case 3: ReqOkay and RabHasBeenLostPd ′ 142 18.10 case 4: ReqOkay and RabEndPd ′ 146 19 Val 149 19.1 Proof obligation 149 19.2 Instantiating lemma 'deterministic' 149 19.3 exists-pd 150 19.4 exists-chosenlost 150 19.5 check-operation 150 19.6 Behaviour of maybeLost and definitelyLost 151 19.7 Clarifying the hypothesis 153 20 Ack 157 20.1 Proof obligation 157 20.2 Instantiating lemma 'deterministic' 157 20.3 exists-pd 158 v 20.4 exists-chosenlost 20.5 check-operation 20.6 Behaviour of maybeLost and definitelyLost 20.7 Finishing proof of check-operation 21 ReadExceptionLog 21.1 Proof obligation 21.2 Invoking lemma 'lost unchanged' 21.3 check-operation-ignore 22 ClearExceptionLog 22.1 Proof obligation 22.2 Invoking lemma 'Lost unchanged' 22.3 check-operation-ignore 23 AuthoriseExLogClear 23.1 Proof obligation 23.2 Proof 24 Archive 24.1 Proof obligation 24.2 Proof III Second Refinement: B to C 25 B to C rules 25.1 Security of the implementation 25.2 Forwards rules proof obligations 26 Rbc 26.1 Retrieve state 27 Initialisation, Finalisation, and Applicability 27.1 Initialisation proof 27.2 Finalisation proof 27.3 Applicability proofs 28 B to C lemmas 28.1 Specialising the proof rules 28.2 Correctness of CIgnore vi 28.3 Correctness of a branch of the operation 182 28.4 Correctness of CIncrease 185 28.5 Correctness of CAbort 185 28.6 Lemma 'logs unchanged' 187 28.7 Lemma 'abort forward': operations that first abort 188 29 Correctness proofs 191 29.1 Introduction 191 29.2 Correctness of CStartFrom 191 29.3 Correctness of CStartTo 193 29.4 Correctness of CReq 196 29.5 Correctness of CVal 197 29.6 Correctness of CAck 198 29.7 Correctness of CReadExceptionLog 200 29.8Correctness of CClearExceptionLog 201 29.9 Correctness of CAuthoriseExLogClear 201 29.10 Correctness of CArchive