org.jmlspecs.samples.jmltutorial
Class Person

java.lang.Object
  org.jmlspecs.samples.jmltutorial.Person

public class Person

extends Object

Class Specifications

public invariant !this.name.equals("")&&this.weight >= 0;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] private  String	name
[spec_public] private  int	weight

 

Constructor Summary

Person(String n)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	addKgs(int kgs)
int	getWeight()
String	toString()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

name

private String name

Specifications: spec_public non_null

weight

private int weight

Specifications: spec_public

Person

public Person(String n)

Specifications:

     also

requires n != null&&!n.equals("");
ensures n.equals(this.name)&&this.weight == 0;

toString

public String toString()

Overrides:

toString in class Object

Specifications:

     also

ensures \result != null&&(* \result is a displayable form of this person *);

     also

ensures \result != null;

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

getWeight

public int getWeight()

Specifications: pure

     also

ensures \result == this.weight;

addKgs

public void addKgs(int kgs)

Specifications:

     also

requires kgs >= 0;
requires this.weight+kgs >= 0;
ensures this.weight == \old(this.weight+kgs);