Go up to Top Go forward to Correctness Proof |
The source code implementing the program is included below. The assertion
NumberOfMessages
states that, as soon as node 0 has signalled by its
variable sent
the initialization of the network, there must be exactly
two messages in the network. A message may be either contained in some channel
out(j)
, or, in a program's local variable msg
.
// -------------------------------------------------------------------------- // $Id: algorithm.tex,v 1.2 1997/11/06 14:37:28 schreine Exp schreine $ // a trivial test application // // (c) 1997, Wolfgang Schreiner <Wolfgang.Schreiner@risc.uni-linz.ac.at> // http://www.risc.uni-linz.ac.at/software/daj // -------------------------------------------------------------------------- import daj.*; // ---------------------------------------------------------------------------- // // the application itself // // ---------------------------------------------------------------------------- public class Main extends Application { // -------------------------------------------------------------------------- // main function of application // -------------------------------------------------------------------------- public static void main(String[] args) { new Main().run(); } // -------------------------------------------------------------------------- // constructor for application // -------------------------------------------------------------------------- public Main() { super("A Trivial Program", 400, 300); } // -------------------------------------------------------------------------- // construction of network // -------------------------------------------------------------------------- public void construct() { Node node0 = node(new Prog(0), "0", 100, 100); Node node1 = node(new Prog(1), "1", 150, 200); Node node2 = node(new Prog(2), "2", 300, 150); link(node0, node1); link(node1, node2); link(node2, node0); link(node0, node2); link(node2, node1); link(node1, node0); } // -------------------------------------------------------------------------- // informative message // -------------------------------------------------------------------------- public String getText() { return "A Trivial Program\n \n" + "2 messages circling bidirectionally\n" + "through a ring of three nodes"; } } // ---------------------------------------------------------------------------- // // a program class // // ---------------------------------------------------------------------------- class Prog extends Program { private int number; public int index; public Message msg; public boolean sent; // -------------------------------------------------------------------------- // called for initialization of program // -------------------------------------------------------------------------- public Prog(int i) { number = i; msg = null; sent = false; } // -------------------------------------------------------------------------- // called for execution of program // -------------------------------------------------------------------------- public void main() { if (number == 0) { out(0).send(new Msg(0)); out(1).send(new Msg(1)); sent = true; } GlobalAssertion assertion = new NumberOfMessages(); for (int i = 0; i < 5; i++) { assert(assertion); index = in().select(); msg = in(index).receive(); out(index).send(msg); msg = null; } } // -------------------------------------------------------------------------- // called for display of program state // -------------------------------------------------------------------------- public String getText() { String msgString; if (msg == null) msgString = "(null)"; else msgString = msg.getText(); return "sent: " + String.valueOf(sent) + "\nmsg: " + msgString; } } // ---------------------------------------------------------------------------- // // a message class // // ---------------------------------------------------------------------------- class Msg extends Message { int val; public Msg(int i) { val = i; } public int value() { return val; } public String getText() { return "content = " + String.valueOf(val); } } // ---------------------------------------------------------------------------- // // global assertion stating that two messages are floating around // // ---------------------------------------------------------------------------- class NumberOfMessages extends GlobalAssertion { int count; public String getText() { return "invalid count of messages: " + String.valueOf(count); } public boolean assert(Program prog[]) { if (!((Prog)prog[0]).sent) return true; count = 0; for (int j = 0; j < prog.length; j++) { Prog program = (Prog)prog[j]; count += getMessages(program.out(0)).length; count += getMessages(program.out(1)).length; if (program.msg != null) count++; } return count == 2; } }