01: /*
02: * JBoss, Home of Professional Open Source.
03: * Copyright 2006, Red Hat Middleware LLC, and individual contributors
04: * as indicated by the @author tags. See the copyright.txt file in the
05: * distribution for a full listing of individual contributors.
06: *
07: * This is free software; you can redistribute it and/or modify it
08: * under the terms of the GNU Lesser General Public License as
09: * published by the Free Software Foundation; either version 2.1 of
10: * the License, or (at your option) any later version.
11: *
12: * This software is distributed in the hope that it will be useful,
13: * but WITHOUT ANY WARRANTY; without even the implied warranty of
14: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15: * Lesser General Public License for more details.
16: *
17: * You should have received a copy of the GNU Lesser General Public
18: * License along with this software; if not, write to the Free
19: * Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
20: * 02110-1301 USA, or see the FSF site: http://www.fsf.org.
21: */
22: package test.dbc.office;
23:
24: import java.util.ArrayList;
25:
26: /**
27: *
28: * @author <a href="mailto:kabir.khan@jboss.org">Kabir Khan</a>
29: * @version $Revision: 57186 $
30: * @@org.jboss.aspects.dbc.Dbc
31: * @@org.jboss.aspects.dbc.Invariant ({"$tgt.computers != null", "$tgt.developers != null", "forall test.dbc.office.Computer c in $tgt.computers | c != null", "forall d in $tgt.developers | d != null"})
32: */
33: public class OfficeManager {
34: ArrayList computers = new ArrayList();
35: ArrayList developers = new ArrayList();
36:
37: /**
38: * PostCond: The computer should be unassigned after adding
39: * @@org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Computer c in $tgt.computers | c.getDeveloper() == null && c == $rtn"})
40: */
41: public Computer createComputer(String name) {
42: Computer computer = new Computer(name);
43: computers.add(computer);
44: return computer;
45: }
46:
47: /**
48: * PostCond: The developer should not have a computer after adding
49: * @@org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Developer d in $tgt.developers | d.getComputer() == null && d == $rtn"})
50: */
51: public Developer createDeveloper(String name) {
52: Developer developer = new Developer(name);
53: developers.add(developer);
54: return developer;
55: }
56:
57: /**
58: * PreCond: The computer and developer must both be not-null, and not previously assigned
59: * PostCond: Make sure that all developers have a computer, and that that computer is
60: * associated with the developer in question
61: *
62: * @@org.jboss.aspects.dbc.PreCond ({"$0 != null", "$1 != null", "exists test.dbc.office.Computer c in $tgt.computers | c.getDeveloper() == null && c == $0", "exists test.dbc.office.Developer d in $tgt.developers | d.getComputer() == null && d == $1"})
63: * @@org.jboss.aspects.dbc.PostCond ({"forall d in $tgt.developers | exists c in $tgt.computers | (c == d.getComputer() && d == c.getDeveloper())"})
64: */
65: public void assignComputer(Computer computer, Developer developer) {
66: System.out
67: .println("========================= SET DEVELOPER ==============================");
68: computer.setDeveloper(developer);
69: System.out
70: .println("========================= SET COMPUTER ==============================");
71: developer.setComputer(computer);
72: }
73:
74: }
|