This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| domains-interference-def-01 | ⊦ domsvar ⇒1 domsvar0 ↔ (∃ domvar, domvar0. domvar ∈ domsvar ∧ domvar0 ∈ domsvar0 ∧ domvar ⇒1 domvar0) | An Axiom |
| User-interference-def-01 | ⊦ User ⇒1 domvar ↔ domvar = User ∨ domvar = User->User_Airline ∨ domvar = Abort9 | An Axiom |
| User_Airline-interference-def-01 | ⊦ User_Airline ⇒1 domvar ↔ domvar = User_Airline ∨ domvar = User ∨ domvar = HighLow5 ∨ domvar = Abort8 | An Axiom |
| User_TravelAgency_Airline-interference-def-01 | ⊦ User_TravelAgency_Airline ⇒1 domvar ↔ domvar = User_TravelAgency_Airline ∨ domvar = User_Airline ∨ domvar = User | An Axiom |
| User-User_Airline-interference-def-01 | ⊦ User->User_Airline ⇒1 domvar ↔ domvar = User->User_Airline ∨ domvar = User_Airline | An Axiom |
| HighLow5-interference-def-01 | ⊦ HighLow5 ⇒1 domvar ↔ domvar = HighLow5 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort8-interference-def-01 | ⊦ Abort8 ⇒1 domvar ↔ domvar = Abort8 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort9-interference-def-01 | ⊦ Abort9 ⇒1 domvar ↔ domvar = Abort9 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| domains-interference-def-02 | ⊦ domsvar ⇒2 domsvar0 ↔ (∃ domvar, domvar0. domvar ∈ domsvar ∧ domvar0 ∈ domsvar0 ∧ domvar ⇒2 domvar0) | An Axiom |
| User-interference-def-02 | ⊦ User ⇒2 domvar ↔ domvar = User ∨ domvar = User->User_Airline ∨ domvar = Abort9 ∨ domvar = User_Airline | An Axiom |
| User_Airline-interference-def-02 | ⊦ User_Airline ⇒2 domvar ↔ domvar = User_Airline ∨ domvar = User ∨ domvar = HighLow5 ∨ domvar = Abort8 ∨ domvar = User->User_Airline | An Axiom |
| User_TravelAgency_Airline-interference-def-02 | ⊦ User_TravelAgency_Airline ⇒2 domvar ↔ domvar = User_TravelAgency_Airline ∨ domvar = User_Airline ∨ domvar = User ∨ domvar = User->User_Airline | An Axiom |
| User-User_Airline-interference-def-02 | ⊦ User->User_Airline ⇒2 domvar ↔ domvar = User->User_Airline ∨ domvar = User_Airline ∨ domvar = User | An Axiom |
| HighLow5-interference-def-02 | ⊦ HighLow5 ⇒2 domvar ↔ domvar = HighLow5 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort8-interference-def-02 | ⊦ Abort8 ⇒2 domvar ↔ domvar = Abort8 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort9-interference-def-02 | ⊦ Abort9 ⇒2 domvar ↔ domvar = Abort9 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| ConfirmIFProperty1 | s(User-ConfirmedRelease-count(`3'), mkUser(0)) = mkNat(0), s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) = mkNat(0), maxOneNotNull(s), s(state(`init'), mkUser(0)) = wrapBoolean2Data(mkBoolean(true)) ⊦ [ASM#(; s, boolvar)] ( s(User-ConfirmedRelease-count(`3'), mkUser(0)) .nat = s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) .nat ∨ s(User-ConfirmedRelease-count(`3'), mkUser(0)) .nat = s(declassify-count(`declassifyCCD'), mkCreditCardCenter(0)) .nat + 1) | An Axiom |
| alter-observe-respects-policy | ⊦ alter(domvar, nam, ag) ∧ observe(domvar0, nam, ag) → domvar ⇒ domvar0 | A Proof Obligation |
| flightOffers-no-read-up | ⊦ observe(domvar, Airline-flightOffers, mkAirline(0)) → dom(Airline-flightOffers, mkAirline(0)) ⇒ domvar | A Proof Obligation |
| flightOffers-no-write-down | ⊦ alter(domvar, Airline-flightOffers, mkAirline(0)) → domvar ⇒ dom(Airline-flightOffers, mkAirline(0)) | A Proof Obligation |
| ccd-no-read-up | ⊦ observe(domvar, CreditCardCenter-ccd, mkCreditCardCenter(n)) → dom(CreditCardCenter-ccd, mkCreditCardCenter(n)) ⇒ domvar | A Proof Obligation |
| ccd-no-write-down | ⊦ alter(domvar, CreditCardCenter-ccd, mkCreditCardCenter(n)) → domvar ⇒ dom(CreditCardCenter-ccd, mkCreditCardCenter(n)) | A Proof Obligation |
| IFProperty1 | ⊦ ¬ ∅ ++ dom(CreditCardCenter-ccd, mkCreditCardCenter(m)) ⇒1 ∅ ++ dom(Mailbox(GetFlightOffers-AirlineCmd), mkAirline(0)) ++ dom(Mailbox(BookFlightOffer-AirlineCmd), mkAirline(0)) ++ dom(Mailbox(OkPayCommission-AirlineCmd), mkAirline(0)) | A Proof Obligation |
| IFProperty2 | ⊦ ¬ ∅ ++ dom(CreditCardCenter-ccd, mkCreditCardCenter(m)) ⇒2 ∅ ++ dom(Mailbox(GetFlightOffers-TravelAgencyCmd), mkTravelAgency(0)) ++ dom(Mailbox(RetFlightOffers-TravelAgencyCmd), mkTravelAgency(0)) ++ dom(Mailbox(PayCommission-TravelAgencyCmd), mkTravelAgency(0)) | A Proof Obligation |