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

Computer

java.lang.Object

public class Computer extends Object

author: Kabir Khan
version: $Revision: 57186 $
@org.jboss.aspects.dbc.Dbc
@org.jboss.aspects.dbc.Invariant: ({"$tgt.name != null"})

Fields Summary
String
name
Developer
developer
Constructors Summary
public Computer(String name)
@org.jboss.aspects.dbc.PreCond
({"$0 != null"})
@org.jboss.aspects.dbc.PostCond
({"$0 == $tgt.name"})
this.name = name;
Methods Summary
public Developer getDeveloper()
@org.jboss.aspects.dbc.PostCond
({"$rtn != null implies ($rtn.getComputer() == null) ||($rtn.getComputer() == $tgt)"})
return developer;
public void setDeveloper(Developer developer)
@org.jboss.aspects.dbc.PostCond
({"$0 == $tgt.getDeveloper()"})
this.developer = developer;