Mail.dfy

/*===============================================
  M.EIC037: Formal Methods For Critical Systems

  Project 2 

  Your name(s): 
  ===============================================*/

include "List.dfy"

import opened L = List

// The next three classes have a minimal class definition,
// for simplicity
class Address
  {
  constructor () {}
}

class Date
  {
  constructor () {}
}

class MessageId
  {
  constructor () {}
}

//==========================================================
//  Message
//==========================================================
class Message
  {
  var id: MessageId
  var content: string
  var date: Date
  var sender: Address
  var recipients: seq<Address>

  constructor (s: Address)
    ensures fresh(id)
    ensures fresh(date)
    ensures content == ""
    ensures sender == s
    ensures recipients == []
  {
    id := new MessageId();
    date := new Date();
    content := "";
    sender := s;
    recipients := [];
  }


  method setContent(c: string)
    modifies this
    ensures content == c
    ensures {id, date, sender} == old({id, date, sender})
    ensures recipients == old(recipients)
  {
    content := c;
  }

  method setDate(d: Date)
    modifies this
    ensures date == d
    ensures {id, sender} == old({id, sender})
    ensures recipients == old(recipients)
    ensures content == old(content)
  {
    date := d;
  }


  method addRecipient(p: nat, r: Address)
    modifies this
    requires p < |recipients|
    ensures |recipients| == |old(recipients)| + 1
    ensures forall i :: 0 <= i < p ==> recipients[i] == old(recipients[i])
    ensures recipients[p] == r
    ensures forall i :: p < i < |recipients| ==> recipients[i] == old(recipients[i-1])
    ensures {id, date, sender} == old({id, date, sender})
    ensures content == old(content)
  {
    recipients := recipients[..p] + [r] + recipients[p..];
  }

}

//==========================================================
//  Mailbox
//==========================================================
//
// Each Mailbox has a name, which is a string.
// Its main content is a set of messages.
//
class Mailbox {
  const name: string
  var messages: set<Message>

  // Class invariant: All messages must be non-null
  // invariant forall m :: m in messages ==> m != null;

  // Creates an empty mailbox with name n
  constructor (n: string)
    ensures name == n
    ensures messages == {}
  {
    name := n;
    messages := {};
  }

  // Adds message m to the mailbox
  method add(m: Message)
    requires m !in messages
    requires m != null
    modifies this
    ensures messages == old(messages) + {m}
    ensures name == old(name)
    ensures m in messages
  {
    messages := { m } + messages;
  }

  // Removes message m from mailbox
  // m need not be in the mailbox
  method remove(m: Message)
    requires m in messages
    modifies this
    ensures messages == old(messages) - {m}
    ensures name == old(name)
    decreases messages
  {
    messages := messages - { m };
  }

  // Empties the mailbox
  method empty()
    modifies this
    ensures messages == {}
    ensures name == old(name)
  {
    messages := {};
  }
}


//==========================================================
//  MailApp
//==========================================================
class MailApp {
  // abstract field for user defined boxes
  ghost var userBoxes: set<Mailbox>

  // abstract function returning all system mailboxes in one set
  ghost function systemBoxes(): set<Mailbox>
    reads this
  { {inbox, drafts, trash, sent} }

  // the inbox, drafts, trash and sent are both abstract and concrete
  var inbox: Mailbox
  var drafts: Mailbox
  var trash: Mailbox
  var sent: Mailbox

  // userboxList implements userBoxes
  var userboxList: List<Mailbox>

  // Class invariant
  ghost predicate isValid()
    reads this
  {
    // replace each `true` by your formulation of the invariants
    // described below
    //----------------------------------------------------------
    // Abstract state invariants
    //----------------------------------------------------------
    // 1. all system mailboxes (inbox, ..., sent) are distinct
    |systemBoxes()| == 4

    //&& true
    // 2. none of the system mailboxes are in the set
    //    of user-defined mailboxes
    && (systemBoxes() * userBoxes == {})
    //----------------------------------------------------------
    // Abstract-to-concrete state invariants
    //----------------------------------------------------------
    // userBoxes is the set of mailboxes in userboxList
    && forall l :: l in elements(userboxList) ==> l in userBoxes && |userBoxes| == |elements(userboxList)|
  }

  constructor ()
    ensures fresh(inbox) && inbox.name == "Inbox"
    ensures fresh(drafts) && drafts.name == "Drafts"
    ensures fresh(trash) && trash.name == "Trash"
    ensures fresh(sent) && sent.name == "Sent"
    ensures inbox.messages == {} && drafts.messages == {} && trash.messages == {} && sent.messages == {}
    ensures len(userboxList) == 0
    ensures fresh(userBoxes)
    ensures isValid()
  {
    inbox := new Mailbox("Inbox");
    drafts := new Mailbox("Drafts");
    trash := new Mailbox("Trash");
    sent := new Mailbox("Sent");
    userboxList := Nil;
    userBoxes := {};
  }

  // Deletes user-defined mailbox mb
  method deleteMailbox(mb: Mailbox)
    requires isValid()
    requires mb !in systemBoxes()
    modifies this
    requires mb in elements(userboxList)
    ensures forall e :: e in elements(userboxList) ==> e != mb
    ensures isValid()
  {
    userboxList := remove(userboxList, mb);
    userBoxes := elements(userboxList);
  }

  // Adds a new mailbox with name n to set of user-defined mailboxes
  // provided that no user-defined mailbox has name n already
  method newMailbox(n: string)
    requires isValid()
    requires forall e :: e in elements(userboxList) ==> e.name != n
    modifies this
    ensures exists mb: Mailbox :: mb in userBoxes && mb.name == n && mb.messages == {}
    ensures exists e :: e in elements(userboxList) ==> e.name == n
    ensures isValid()
  {
    var mb := new Mailbox(n);
    userboxList := Cons(mb, userboxList);
    userBoxes := elements(userboxList);
  }

  // Adds a new message with sender s to the drafts mailbox
  method newMessage(s: Address)
    requires isValid()
    modifies this, drafts
    ensures |old(drafts.messages)| + 1 == |drafts.messages|
    ensures isValid()
    ensures exists nw: Message :: nw in drafts.messages
    ensures old(drafts.messages) == {} ==> exists nw: Message :: drafts.messages == {nw}
  {
    var m := new Message(s);
    drafts.add(m);
  }

  // Moves message m from mailbox mb1 to a different mailbox mb2
  method moveMessage (m: Message, mb1: Mailbox, mb2: Mailbox)
    requires isValid()
    requires m in mb1.messages && !(m in mb2.messages)
    modifies mb1, mb2
    ensures m in mb2.messages && !(m in mb1.messages)
    ensures isValid()
  {
    mb1.remove(m);
    mb2.add(m);
  }

  // Moves message m from non-null mailbox mb to the trash mailbox
  // provided that mb is not the trash mailbox
  method deleteMessage (m: Message, mb: Mailbox)
    requires isValid()
    requires m in mb.messages && m !in trash.messages
    modifies mb, trash
    ensures m !in mb.messages && m in trash.messages
    ensures isValid()
  {
    moveMessage(m, mb, trash);
  }

  // Moves message m from the drafts mailbox to the sent mailbox
  method sendMessage(m: Message)
    requires isValid()
    requires m in drafts.messages && m !in sent.messages
    modifies drafts, sent
    ensures m in sent.messages && m !in drafts.messages
    ensures isValid()
  {
    moveMessage(m, drafts, sent);
  }

  // Empties the trash mailbox
  method emptyTrash ()
    requires isValid()
    modifies trash
    ensures trash.messages == {}
    ensures isValid()
  {
    trash.empty();
  }
}

// Test
/* Can be used to test your code. */

method test() {

  var ma := new MailApp();
  assert ma.inbox.name == "Inbox";
  assert ma.drafts.name == "Drafts";
  assert ma.trash.name == "Trash";
  assert ma.sent.name == "Sent";
  assert ma.inbox.messages == ma.drafts.messages ==
         ma.trash.messages ==
         ma.sent.messages == {};

  ma.newMailbox("students");
  assert exists mb: Mailbox :: mb in ma.userBoxes && mb.name == "students" && mb.messages == {};

  var s := new Address();

  ma.newMessage(s);

  assert exists nw: Message :: ma.drafts.messages == {nw};
}