File	Doc	Category	Size	Date	Package
OfficeManager.java	API Doc	JBoss 4.2.1	3334	Fri Jul 13 21:02:22 BST 2007	test.dbc.office

OfficeManager

• java.lang.Object

Fields Summary
ArrayList	computers
ArrayList	developers

Constructors Summary

Methods Summary
public void	assignComputer(Computer computer, Developer developer) PreCond: The computer and developer must both be not-null, and not previously assigned PostCond: Make sure that all developers have a computer, and that that computer is associated with the developer in question @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"}) @org.jboss.aspects.dbc.PostCond ({"forall d in $tgt.developers | exists c in $tgt.computers | (c == d.getComputer() && d == c.getDeveloper())"}) System.out.println("========================= SET DEVELOPER =============================="); computer.setDeveloper(developer); System.out.println("========================= SET COMPUTER =============================="); developer.setComputer(computer);
public Computer	createComputer(java.lang.String name) PostCond: The computer should be unassigned after adding @org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Computer c in $tgt.computers | c.getDeveloper() == null && c == $rtn"}) Computer computer = new Computer(name); computers.add(computer); return computer;
public Developer	createDeveloper(java.lang.String name) PostCond: The developer should not have a computer after adding @org.jboss.aspects.dbc.PostCond ({"exists test.dbc.office.Developer d in $tgt.developers | d.getComputer() == null && d == $rtn"}) Developer developer = new Developer(name); developers.add(developer); return developer;