Java Software Development with Event B by Néstor Cataño Collazos & Luciano Baresi

Author:Néstor Cataño Collazos & Luciano Baresi [Néstor Cataño Collazos]
Language: eng
Format: epub
Publisher: Morgan & Claypool Publishers
Published: 2020-01-26T16:00:00+00:00

We present below the encoding of US-04a and US-04b; therefore, delete-content removes content c from the chat u1↦u2, and remove-content from everywhere. Notice that delete-content does not remove c from chat u2↦u1. Guard @grd2 verifies that the user u1 who deletes or removes the content is actively chatting with u2. delete-content uses the functional overriding operator ⊗ to override u1’s chat content. It removes u2 from chatcontent(u1)(c) so that u2 no longer appears as having received content c from u1.

remove-content uses the domain subtraction operator ⩤ to remove content c from every user to whom u1 sent the said content.

Notice that if u1 is chatting with u2, and u2 with u3, and u1 sends c to u2, and u2 sends c to u3, calling remove-content with parameters u1, u2, and c does not remove c from the chat between u2 and u3, but only from the chat between u1 and u2 and between u2 and u1. For this very reason, remove-content does not implement a second action @act2 content ≔ content ∖ {c}.

Download

Copyright Disclaimer:
This site does not store any files on its server. We only index and link to content provided by other sites. Please contact the content providers to delete copyright contents if any and email us, we'll remove relevant links or contents immediately.