KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > test > dbc > office > OfficeManager


1 /*
2 * JBoss, Home of Professional Open Source
3 * Copyright 2005, JBoss Inc., and individual contributors as indicated
4 * by the @authors tag. See the copyright.txt in the distribution for a
5 * full listing of individual contributors.
6 *
7 * This is free software; you can redistribute it and/or modify it
8 * under the terms of the GNU Lesser General Public License as
9 * 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 JavaDoc;
25
26 /**
27  *
28  * @author <a HREF="mailto:kabir.khan@jboss.org">Kabir Khan</a>
29  * @version $Revision: 37406 $
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 {
35    ArrayList JavaDoc computers = new ArrayList JavaDoc();
36    ArrayList JavaDoc developers = new ArrayList JavaDoc();
37    
38    /**
39     * PostCond: The computer should be unassigned after adding
40     * @@org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Computer c in $tgt.computers | c.getDeveloper() == null && c == $rtn"})
41     */
42    public Computer createComputer(String JavaDoc name)
43    {
44       Computer computer = new Computer(name);
45       computers.add(computer);
46       return computer;
47    }
48    
49    /**
50     * PostCond: The developer should not have a computer after adding
51     * @@org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Developer d in $tgt.developers | d.getComputer() == null && d == $rtn"})
52     */
53    public Developer createDeveloper(String JavaDoc name)
54    {
55       Developer developer = new Developer(name);
56       developers.add(developer);
57       return developer;
58    }
59    
60    /**
61     * PreCond: The computer and developer must both be not-null, and not previously assigned
62     * PostCond: Make sure that all developers have a computer, and that that computer is
63     * associated with the developer in question
64     *
65     * @@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"})
66     * @@org.jboss.aspects.dbc.PostCond ({"forall d in $tgt.developers | exists c in $tgt.computers | (c == d.getComputer() && d == c.getDeveloper())"})
67     */
68    public void assignComputer(Computer computer, Developer developer)
69    {
70       System.out.println("========================= SET DEVELOPER ==============================");
71       computer.setDeveloper(developer);
72       System.out.println("========================= SET COMPUTER ==============================");
73       developer.setComputer(computer);
74    }
75    
76 }
77
Popular Tags