--> inv4 --> initial states --> init open INV ops d1 d2 : -> DocumentID . red inv4(init, d1, d2) . close -- --> ************************************************* --> 1. Create-cc-order : SaleAndShip SessionID DocumentID --> -> SaleAndShip --> 1.1 c-Create-cc-order(s, i, d1, d2) --> 1.1.1 d1 = d2, d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Create-cc-order(s, i, d1) = true . -- c-Create-cc-order(s, i, d1) -- = (s = init) eq s = init . -- eq d2 = d1 . eq d3 = d1 . -- successor state eq s' = Create-cc-order(s, i, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . close -- --> ================================================= --> 1.1.2 d1 = d2, ~(d1 = d3) open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Create-cc-order(s, i, d1) = true . -- c-Create-cc-order(s, i, d1) -- = (s = init) eq s = init . -- eq d2 = d1 . eq (d3 = d1) = false . -- successor state eq s' = Create-cc-order(s, i, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . close -- --> ================================================= --> 1.1.3 ~(d1 = d2), d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Create-cc-order(s, i, d1) = true . -- c-Create-cc-order(s, i, d1) -- = (s = init) eq s = init . -- eq (d2 = d1) = false . eq d3 = d1 . -- successor state eq s' = Create-cc-order(s, i, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 1.1.4 ~(d1 = d2), ~(d1 = d3) --> 1.1.4.1 cc(d1) = d2 open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Create-cc-order(s, i, d1) = true . -- c-Create-cc-order(s, i, d1) -- = (s = init) eq s = init . -- eq (d2 = d1) = false . eq (d3 = d1) = false . -- eq d2 = cc(d1) . -- -- successor state eq s' = Create-cc-order(s, i, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 1.1.4.2 ~(cc(d1) = d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Create-cc-order(s, i, d1) = true . -- c-Create-cc-order(s, i, d1) -- = (s = init) eq s = init . -- eq (d2 = d1) = false . eq (d3 = d1) = false . -- eq (d2 = cc(d1)) = false . -- -- successor state eq s' = Create-cc-order(s, i, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 1.2 ~c-Create-cc-order(s, i, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . op i : -> SessionID . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Create-cc-order(s, i, d1) = false . -- -- successor state eq s' = Create-cc-order(s, i, d1) . -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 2. Send-order : SaleAndShip DocumentID -> SaleAndShip --> 2.1 c-Send-order(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-order(s, d1) = true . -- c-Send-order(s, d1) -- = c-Send(s, client, d1, sales) and -- (DocumentType(s, d1) = order) . eq Place(s, d1) = client . eq DocumentType(s, d1) = order . -- -- successor state eq s' = Send-order(s, d1) . -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 2.2 ~c-Send-order(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-order(s, d1) = false . -- -- successor state eq s' = Send-order(s, d1) . -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 3. Create-receipt : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 3.1 c-Create-receipt(s, d1, d2) --> 3.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op h : -> EvidenceHistory . -- assumption -- eq c-Create-receipt(s, d1, d2) = true . -- c-Create-receipt(s, d1, d2) -- = c-Create-2(s, client, d1, receipt, d2) and -- (DocumentType(s, d2) = invoice) and -- (DocumentIDList(s, SessionID(s, d2), receipt) = -- nillDID) and -- in?(ch(cc(order)), -- Evidences(s, d2)) . eq Place(s, d1) = noDivision . eq Place(s, d2) = client . eq DocumentType(s, d2) = invoice . eq DocumentIDList(s, SessionID(s, d2), receipt) = nillDID . -- in?(ch(cc(order)), Evidences(s, d2)) eq Evidences(s, d2) = (ch(cc(order)) h) . -- eq d3 = d1 . -- -- successor state eq s' = Create-receipt(s, d1, d2) . -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 3.1.2 ~(d1 = d3) --> 3.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op h : -> EvidenceHistory . -- assumption -- eq c-Create-receipt(s, d1, d2) = true . -- c-Create-receipt(s, d1, d2) -- = c-Create-2(s, client, d1, receipt, d2) and -- (DocumentType(s, d2) = invoice) and -- (DocumentIDList(s, SessionID(s, d2), receipt) = -- nillDID) and -- in?(ch(cc(order)), -- Evidences(s, d2)) . eq Place(s, d1) = noDivision . eq Place(s, d2) = client . eq DocumentType(s, d2) = invoice . eq DocumentIDList(s, SessionID(s, d2), receipt) = nillDID . -- in?(ch(cc(order)), Evidences(s, d2)) eq Evidences(s, d2) = (ch(cc(order)) h) . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Create-receipt(s, d1, d2) . -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 3.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op h : -> EvidenceHistory . -- assumption -- eq c-Create-receipt(s, d1, d2) = true . -- c-Create-receipt(s, d1, d2) -- = c-Create-2(s, client, d1, receipt, d2) and -- (DocumentType(s, d2) = invoice) and -- (DocumentIDList(s, SessionID(s, d2), receipt) = -- nillDID) and -- in?(ch(cc(order)), -- Evidences(s, d2)) . eq Place(s, d1) = noDivision . eq Place(s, d2) = client . eq DocumentType(s, d2) = invoice . eq DocumentIDList(s, SessionID(s, d2), receipt) = nillDID . -- in?(ch(cc(order)), Evidences(s, d2)) eq Evidences(s, d2) = (ch(cc(order)) h) . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Create-receipt(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 3.2 ~c-Create-receipt(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Create-receipt(s, d1, d2) = false . -- -- successor state eq s' = Create-receipt(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 4. Send-receipt : SaleAndShip DocumentID -> SaleAndShip --> 4.1 c-Send-receipt(s) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-receipt(s, d1) = true . -- c-Send-receipt(s, d1) -- = c-Send(S, client, d1, sales) and -- (DocumentType(S, D) = receipt) . eq Place(s, d1) = client . eq DocumentType(s, d1) = receipt . -- -- successor state eq s' = Send-receipt(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 4.2 ~c-Send-receipt(s) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-receipt(s, d1) = false . -- -- successor state eq s' = Send-receipt(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 5. Check-ack : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 5.1 c-Check-ack(s, d1, d2) --> 5.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-ack(s, d1, d2) = true . -- c-Check-ack(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = ack) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = ack . eq DocumentType(s, d2) = cc(order) . -- eq d3 = d1 . -- -- successor state eq s' = Check-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 5.1.2 ~(d1 = d3) --> 5.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-ack(s, d1, d2) = true . -- c-Check-ack(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = ack) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = ack . eq DocumentType(s, d2) = cc(order) . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Check-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 5.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-ack(s, d1, d2) = true . -- c-Check-ack(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = ack) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = ack . eq DocumentType(s, d2) = cc(order) . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Check-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 5.2 ~c-Check-ack(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Check-ack(s, d1, d2) = false . -- -- successor state eq s' = Check-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 6. Check-invoice : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 6.1 c-Check-invoice(s, d1, d2) --> 6.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-invoice(s, d1, d2) = true . -- c-Check-invoice(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = invoice) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = invoice . eq DocumentType(s, d2) = cc(order) . -- eq d3 = d1 . -- -- successor state eq s' = Check-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 6.1.2 ~(d1 = d3) --> 6.1.2.1 d1 = d4 --> 6.1.2.1.1 Legal?(s, d1) = Legal?(s, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-invoice(s, d1, d2) = true . -- c-Check-invoice(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = invoice) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = invoice . eq DocumentType(s, d2) = cc(order) . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- eq Legal?(s, d2) = Legal?(s, d1) . -- -- successor state eq s' = Check-invoice(s, d1, d2) . -- -- check red inv6(s, d3, d2, d4) implies (inv4(s, d3, d4) implies inv4(s', d3, d4)) . -- close -- --> ================================================= --> 6.1.2.1.2 ~(Legal?(s, d1) = Legal?(s, d2)) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-invoice(s, d1, d2) = true . -- c-Check-invoice(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = invoice) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = invoice . eq DocumentType(s, d2) = cc(order) . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- eq (Legal?(s, d2) = Legal?(s, d1)) = false . -- -- successor state eq s' = Check-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 6.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-invoice(s, d1, d2) = true . -- c-Check-invoice(s, d1, d2) -- = c-Check-1(s, client, d1, d2) and -- (DocumentType(s, d1) = invoice) and -- (DocumentType(s, d2) = cc(order)) . eq Place(s, d1) = client . eq Place(s, d2) = client . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = invoice . eq DocumentType(s, d2) = cc(order) . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Check-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 6.2 ~c-Check-invoice(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Check-invoice(s, d1, d2) = false . -- -- successor state eq s' = Check-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 7. Create-ack : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 7.1 c-Create-ack(s, d1, d2) --> 7.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-ack(s, d1, d2) = true . -- c-Create-ack(s, d1, d2) -- = c-Create-2(s, sales, d1, d2) and -- (DocumentType(S, D2) = order) and -- (DocumentIDList(S, SessionID(S, D2), ack) = -- nillDID) and -- (Evidences(S, D2) = emptyE) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), ack) = nillDID . eq Evidences(s, d2) = emptyE . -- eq d3 = d1 . -- -- successor state eq s' = Create-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 7.1.2 ~(d1 = d3) --> 7.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-ack(s, d1, d2) = true . -- c-Create-ack(s, d1, d2) -- = c-Create-2(s, sales, d1, d2) and -- (DocumentType(s, d2) = order) and -- (DocumentIDList(S, SessionID(s, d2), ack) = -- nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), ack) = nillDID . eq Evidences(s, d2) = emptyE . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Create-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 7.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-ack(s, d1, d2) = true . -- c-Create-ack(s, d1, d2) -- = c-Create-2(s, sales, d1, d2) and -- (DocumentType(s, d2) = order) and -- (DocumentIDList(S, SessionID(s, d2), ack) = -- nillDID) and -- (Evidences(s, d2) = emptyE) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), ack) = nillDID . eq Evidences(s, d2) = emptyE . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Create-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 7.2 ~c-Create-ack(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Create-ack(s, d1, d2) = false . -- -- successor state eq s' = Create-ack(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 8. Send-ack : SaleAndShip DocumentID -> SaleAndShip --> 8.1 c-Send-ack(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-ack(s) = true . -- c-Send-ack(s) = c-Send(s, sales, d1, client) and -- (DocumentType(s, d1) = ack) . eq Place(s, d1) = sales . eq DocumentType(s, d1) = ack . -- -- successor state eq s' = Send-ack(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 8.2 ~c-Send-ack(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-ack(s, d1) = false . -- -- successor state eq s' = Send-ack(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 9. Create-request : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 9.1 c-Create-request(s, d1, d2) --> 9.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op h : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-request(s, d1, d2) = true . -- c-Create-request(s, d1, d2) -- = c-Create-2(s, sales, d1, request, d2) and -- (DocumentType(s, d2) = order) and -- (DocumentIDList(S, SessionID(S, D2), request) -- = nillDID) and -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), request) = nillDID . -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) eq DocumentIDList(s, SessionID(s, d2), ack) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(cc(order)) h) . -- eq d3 = d1 . -- -- successor state eq s' = Create-request(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 9.1.2 ~(d1 = d3) --> 9.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op h : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-request(s, d1, d2) = true . -- c-Create-request(s, d1, d2) -- = c-Create-2(s, sales, d1, request, d2) and -- (DocumentType(s, d2) = order) and -- (DocumentIDList(S, SessionID(S, D2), request) -- = nillDID) and -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), request) = nillDID . -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) eq DocumentIDList(s, SessionID(s, d2), ack) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(cc(order)) h) . -- eq (d3 = d1) = false . -- eq (d1 = d4) = true . -- -- successor state eq s' = Create-request(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 9.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op h : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-request(s, d1, d2) = true . -- c-Create-request(s, d1, d2) -- = c-Create-2(s, sales, d1, request, d2) and -- (DocumentType(s, d2) = order) and -- (DocumentIDList(S, SessionID(S, D2), request) -- = nillDID) and -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) . eq Place(s, d1) = noDivision . eq Place(s, d2) = sales . eq DocumentType(s, d2) = order . eq DocumentIDList(s, SessionID(s, d2), request) = nillDID . -- in?(ch(cc(order)), -- Evidences(s, -- top(DocumentIDList(s, -- SessionID(s, d2)), -- ack))) eq DocumentIDList(s, SessionID(s, d2), ack) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(cc(order)) h) . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Create-request(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 9.2 ~c-Create-request(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Create-request(s, d1, d2) = false . -- -- successor state eq s' = Create-request(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 10. Send-request : SaleAndShip DocumentID -> SaleAndShip --> 10.1 c-Send-request(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-request(s, d1) = true . -- c-Send-request(s, d1) -- = c-Send(s, sales, d1, shipping) and -- (DocumentType(s, d1) = request) . eq Place(s, d1) = sales . eq DocumentType(s, d1) = request . -- -- successor state eq s' = Send-request(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 10.2 ~c-Send-request(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-request(s, d1) = false . -- -- successor state eq s' = Send-request(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 11. Approve-order : SaleAndShip DocumentID -> SaleAndShip --> 11.1 c-Approve-order(s, d1) --> 11.1.1 d1 = d2, d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Approve-order(s, d1) = true . -- c-Approve-order(s, d1) -- = c-Approve-1(s, sales, d1) and -- (DocumentType(s, d1) = order) and -- (Evidences(s, d1) = emptyE) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . -- eq Place(s, d1) = sales . eq DocumentType(s, d1) = order . eq Evidences(s, d1) = emptyE . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . eq DocumentIDList(s, SessionID(s, d1), ack) = (d4 ; dlist) . eq Place(s, d4) = sales . -- eq d2 = d1 . eq d3 = d1 . -- -- successor state eq s' = Approve-order(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 11.1.2 d1 = d2, ~(d1 = d3), inv7 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op i : -> SessionID . op dlist : -> DocumentIDList . -- single session eq SessionID(s, d1) = i . eq SessionID(s, d2) = i . eq SessionID(s, d3) = i . eq SessionID(s, d4) = i . -- assumption -- eq c-Approve-order(s, d1) = true . -- c-Approve-order(s, d1) -- = c-Approve-1(s, sales, d1) and -- (DocumentType(s, d1) = order) and -- (Evidences(s, d1) = emptyE) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . -- eq Place(s, d1) = sales . eq DocumentType(s, d1) = order . eq Evidences(s, d1) = emptyE . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . eq DocumentIDList(s, i, ack) = (d4 ; dlist) . eq Place(s, d4) = sales . -- eq d2 = d1 . eq (d3 = d1) = false . -- -- eq (DocumentType(s, d3) = invoice) = false . -- successor state eq s' = Approve-order(s, d1) . -- check red inv7(s, i, d4, d3) implies (inv4(s, d2, d3) implies inv4(s', d2, d3)) . close -- --> ================================================= --> 11.1.3 ~(d1 = d2), d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Approve-order(s, d1) = true . -- c-Approve-order(s, d1) -- = c-Approve-1(s, sales, d1) and -- (DocumentType(s, d1) = order) . -- (Evidences(s, d1) = emptyE) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . -- eq Place(s, d1) = sales . eq DocumentType(s, d1) = order . eq Evidences(s, d1) = emptyE . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . eq DocumentIDList(s, SessionID(s, d1), ack) = (d4 ; dlist) . eq Place(s, d4) = sales . -- eq (d2 = d1) = false . eq d3 = d1 . -- -- successor state eq s' = Approve-order(s, d1) . -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . close -- --> ================================================= --> 11.1.4 ~(d1 = d2), ~(d1 = d3) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Approve-order(s, d1) = true . -- c-Approve-order(s, d1) -- = c-Approve-1(s, sales, d1) and -- (DocumentType(s, d1) = order) . -- (Evidences(s, d1) = emptyE) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . -- eq Place(s, d1) = sales . eq DocumentType(s, d1) = order . eq Evidences(s, d1) = emptyE . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d1), -- ack))) = -- sales) . eq DocumentIDList(s, SessionID(s, d1), ack) = (d4 ; dlist) . eq Place(s, d4) = sales . -- eq (d2 = d1) = false . eq (d3 = d1) = false . -- -- successor state eq s' = Approve-order(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 11.2 ~c-Approve-order(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Approve-order(s, d1) = false . -- -- successor state eq s' = Approve-order(s, d1) . -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . close -- --> ************************************************* --> 12. Check-receipt : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 12.1 c-Check-receipt(s, d1, d2) --> 12.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-receipt(s, d1, d2) = true . -- c-Check-receipt(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = receipt) and -- (DocumentType(s, d2) = order) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = receipt . eq DocumentType(s, d2) = order . -- eq d3 = d1 . -- -- successor state eq s' = Check-receipt(s, d1, d2) . -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . close -- --> ================================================= --> 12.1.2 ~(d1 = d3) --> 12.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-receipt(s, d1, d2) = true . -- c-Check-receipt(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = receipt) and -- (DocumentType(s, d2) = order) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = receipt . eq DocumentType(s, d2) = order . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Check-receipt(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 12.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Check-receipt(s, d1, d2) = true . -- c-Check-receipt(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = receipt) and -- (DocumentType(s, d2) = order) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = receipt . eq DocumentType(s, d2) = order . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Check-receipt(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 12.2 ~c-Check-receipt(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Check-receipt(s, d1, d2) = false . -- -- successor state eq s' = Check-receipt(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 13. Check-report : SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 13.1 c-Check-report(s, d1, d2) --> 13.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . ops h1 h2 : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Check-report(s, d1, d2) = true . -- c-Check-report(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = report) and -- (DocumentType(s, d2) = order) and -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = report . eq DocumentType(s, d2) = order . -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq DocumentIDList(s, SessionID(s, d1), receipt) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(order) h1) . -- eq d3 = d1 . -- -- successor state eq s' = Check-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 13.1.2 ~(d1 = d3) --> 13.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . ops h1 h2 : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Check-report(s, d1, d2) = true . -- c-Check-report(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = report) and -- (DocumentType(s, d2) = order) and -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = report . eq DocumentType(s, d2) = order . -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq DocumentIDList(s, SessionID(s, d1), receipt) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(order) h1) . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Check-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 13.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . ops h1 h2 : -> EvidenceHistory . op dlist : -> DocumentIDList . -- assumption -- eq c-Check-report(s, d1, d2) = true . -- c-Check-report(s, d1, d2) -- = c-Check-3(s, sales, d1, d2, apv(sales)) and -- (DocumentType(s, d1) = report) and -- (DocumentType(s, d2) = order) and -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq Place(s, d1) = sales . eq Place(s, d2) = sales . eq SessionID(s, d2) = SessionID(s, d1) . eq DocumentType(s, d1) = report . eq DocumentType(s, d2) = order . -- in?(ch(order), -- Evidences(s, DocumentID(s, -- SessionID(s, d1), -- receipt))) . eq DocumentIDList(s, SessionID(s, d1), receipt) = (d5 ; dlist) . eq Evidences(s, d5) = (ch(order) h1) . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Check-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 13.2 ~c-Check-report(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Check-report(s, d1, d2) = false . -- -- successor state eq s' = Check-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 14. Create-cc-invoice : --> SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 14.1 c-Create-cc-invoice(s, d1, d2) --> 14.1.1 d3 = d1 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-cc-invoice(s, d1, d2) -- c-Create-cc-invoice(s, d1, d2) -- = c-Create-cc-2(s, shipping, d1, invoice, d2) and -- (DocumentType(s, d2) = request) . -- (DocumentIDList(s, SessionID(s, d2), invoice) -- = nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = shipping . eq DocumentType(s, d2) = request . eq DocumentIDList(s, SessionID(s, d2), invoice) = nillDID . -- eq d3 = d1 . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 14.1.2 ~(d3 = d1) --> 14.1.2.1 d3 = cc(d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-cc-invoice(s, d1, d2) -- c-Create-cc-invoice(s, d1, d2) -- = c-Create-cc-2(s, shipping, d1, invoice, d2) and -- (DocumentType(s, d2) = request) . -- (DocumentIDList(s, SessionID(s, d2), invoice) -- = nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = shipping . eq DocumentType(s, d2) = request . eq DocumentIDList(s, SessionID(s, d2), invoice) = nillDID . -- eq (d3 = d1) = false . -- eq d3 = cc(d1) . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 14.1.2.2 ~(d3 = cc(d1)) --> 14.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-cc-invoice(s, d1, d2) -- c-Create-cc-invoice(s, d1, d2) -- = c-Create-cc-2(s, shipping, d1, invoice, d2) and -- (DocumentType(s, d2) = request) . -- (DocumentIDList(s, SessionID(s, d2), invoice) -- = nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = shipping . eq DocumentType(s, d2) = request . eq DocumentIDList(s, SessionID(s, d2), invoice) = nillDID . -- eq (d3 = d1) = false . -- eq (d3 = cc(d1)) = false . -- eq d4 = d1 . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 14.1.2.2 ~(d1 = d4) --> 14.1.2.2.1 cc(d1) = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-cc-invoice(s, d1, d2) -- c-Create-cc-invoice(s, d1, d2) -- = c-Create-cc-2(s, shipping, d1, invoice, d2) and -- (DocumentType(s, d2) = request) . -- (DocumentIDList(s, SessionID(s, d2), invoice) -- = nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = shipping . eq DocumentType(s, d2) = request . eq DocumentIDList(s, SessionID(s, d2), invoice) = nillDID . -- eq (d3 = d1) = false . -- eq (d3 = cc(d1)) = false . -- eq (d4 = d1) = false . -- eq d4 = cc(d1) . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 14.1.2.2.2 cc(d1) = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption -- eq c-Create-cc-invoice(s, d1, d2) -- c-Create-cc-invoice(s, d1, d2) -- = c-Create-cc-2(s, shipping, d1, invoice, d2) and -- (DocumentType(s, d2) = request) . -- (DocumentIDList(s, SessionID(s, d2), invoice) -- = nillDID) . eq Place(s, d1) = noDivision . eq Place(s, d2) = shipping . eq DocumentType(s, d2) = request . eq DocumentIDList(s, SessionID(s, d2), invoice) = nillDID . -- eq (d3 = d1) = false . -- eq (d3 = cc(d1)) = false . -- eq (d4 = d1) = false . -- eq (d4 = cc(d1)) = false . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . close -- --> ================================================= --> 14.2 ~c-Create-cc-invoice(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Create-cc-invoice(s, d1, d2) = false . -- -- successor state eq s' = Create-cc-invoice(s, d1, d2) . -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . close -- --> ************************************************* --> 15. Send-invoice(S, D) : SaleAndShip DocumentID --> -> SaleAndShip --> 15.1 c-Send-invoice(S, D) = true open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-invoice(s, d1) -- c-Send-invoice(s, d1) -- = c-Send(s, shipping, d1, client) and -- (DocumentType(s, d1) = invoice) . eq Place(s, d1) = shipping . eq DocumentType(s, d1) = invoice . -- -- successor state eq s' = Send-invoice(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 15.2 ~c-Send-invoice(S, D) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-invoice(s, d1) = false . -- -- successor state eq s' = Send-invoice(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 16. Create-report : --> SaleAndShip DocumentID DocumentID --> -> SaleAndShip --> 16.1 c-Create-report(s, d1, d2) --> 16.1.1 d3 = d1 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-report(s, d1, d2) -- c-Create-report(s, d1, d2) -- = c-Create-2(s, shipping, d1, report, d2) and -- (DocumentType(s, d2) = cc(invoice)) and -- (DocumentIDList(s, SessionID(s, d2), report) -- = nillDID) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq Place(s, d1) = noDivision . eq Place(S, d2) = shipping . eq DocumentType(s, d2) = cc(invoice) . eq DocumentIDList(s, SessionID(s, d2), report) = nillDID . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq DocumentIDList(s, SessionID(s, d2), invoice) = (d5 ; dlist) . eq Place(s, d5) = client . -- eq d3 = d1 . -- -- successor state eq s' = Create-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 16.1.2 ~(d3 = d1) --> 16.1.2.1 d1 = d4 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-report(s, d1, d2) -- c-Create-report(s, d1, d2) -- = c-Create-2(s, shipping, d1, report, d2) and -- (DocumentType(s, d2) = cc(invoice)) and -- (DocumentIDList(s, SessionID(s, d2), report) -- = nillDID) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq Place(s, d1) = noDivision . eq Place(S, d2) = shipping . eq DocumentType(s, d2) = cc(invoice) . eq DocumentIDList(s, SessionID(s, d2), report) = nillDID . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq DocumentIDList(s, SessionID(s, d2), invoice) = (d5 ; dlist) . eq Place(s, d5) = client . -- eq (d3 = d1) = false . -- eq d4 = d1 . -- -- successor state eq s' = Create-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 16.1.2.2 ~(d1 = d4) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 d5 : -> DocumentID . op dlist : -> DocumentIDList . -- assumption -- eq c-Create-report(s, d1, d2) -- c-Create-report(s, d1, d2) -- = c-Create-2(s, shipping, d1, report, d2) and -- (DocumentType(s, d2) = cc(invoice)) and -- (DocumentIDList(s, SessionID(s, d2), report) -- = nillDID) and -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq Place(s, d1) = noDivision . eq Place(S, d2) = shipping . eq DocumentType(s, d2) = cc(invoice) . eq DocumentIDList(s, SessionID(s, d2), report) = nillDID . -- (Place(s, -- top(DocumentIDList(s, -- SessionID(s, d2), -- invoice))) -- = client) . eq DocumentIDList(s, SessionID(s, d2), invoice) = (d5 ; dlist) . eq Place(s, d5) = client . -- eq (d3 = d1) = false . -- eq (d4 = d1) = false . -- -- successor state eq s' = Create-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ================================================= --> 16.2 ~c-Create-report(s, d1, d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 d4 : -> DocumentID . -- assumption eq c-Create-report(s, d1, d2) = false . -- -- successor state eq s' = Create-report(s, d1, d2) . -- -- check red inv4(s, d3, d4) implies inv4(s', d3, d4) . -- close -- --> ************************************************* --> 17. Send-report : --> SaleAndShip DocumentID -> SaleAndShip --> 17.1 c-Send-report(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Send-report(s, d1) -- c-Send-report(s, d1) -- = c-Send(s, shipping, d1, sales) and -- (DocumentType(S, d1) = report) . eq Place(s, d1) = shipping . eq DocumentType(s, d1) = report . -- -- successor state eq s' = Send-report(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 17.2 ~c-Send-report(s, d1) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Send-report(s, d1) = false . -- -- successor state eq s' = Send-report(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* --> 18. Forge-SaleAndShip : --> SaleAndShip DocumentID -> Bool --> 18.1 c-Forge-SaleAndShip --> 18.1.1 d1 = d3 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Forge-SaleAndShip(s, d1) -- c-Forge-SaleAndShip(s, d1) -- = c-Forge-SaleAndShip(s, d1) eq in?(Place(s, d1), UntrustedSet(s)) = true . -- eq d3 = d1 . -- -- successor state eq s' = Forge-SaleAndShip(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 18.1.2 ~(d1 = d3) --> 18.1.2.1 d1 = d2 open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Forge-SaleAndShip(s, d1) -- c-Forge-SaleAndShip(s, d1) -- = c-Forge-SaleAndShip(s, d1) eq in?(Place(s, d1), UntrustedSet(s)) = true . -- eq (d3 = d1) = false . -- eq d2 = d1 . -- -- successor state eq s' = Forge-SaleAndShip(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 18.1.2.2 ~(d1 = d2) open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption -- eq c-Forge-SaleAndShip(s, d1) -- c-Forge-SaleAndShip(s, d1) -- = c-Forge-SaleAndShip(s, d1) eq in?(Place(s, d1), UntrustedSet(s)) = true . -- eq (d3 = d1) = false . -- eq (d2 = d1) = false . -- -- successor state eq s' = Forge-SaleAndShip(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ================================================= --> 18.2 ~c-Forge-SaleAndShip open INV -- arbitrary objects ops s s' : -> SaleAndShip . ops d1 d2 d3 : -> DocumentID . -- assumption eq c-Forge-SaleAndShip(s, d1) = false . -- -- successor state eq s' = Forge-SaleAndShip(s, d1) . -- -- check red inv4(s, d2, d3) implies inv4(s', d2, d3) . -- close -- --> ************************************************* eof