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

Developer

java.lang.Object

public class Developer 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
Computer
computer
Constructors Summary
public Developer(String name)
@org.jboss.aspects.dbc.PreCond
({"$0 != null"})
@org.jboss.aspects.dbc.PostCond
({"$0 == $tgt.name"})
this.name = name;
Methods Summary
public Computer getComputer()
@org.jboss.aspects.dbc.PostCond
({"$rtn != null implies ($rtn.getDeveloper() == null) ||($rtn.getDeveloper() == $tgt)"})
return computer;
public void setComputer(Computer computer)
@org.jboss.aspects.dbc.PostCond
({"$0 == $tgt.getComputer()"})
this.computer = computer;