org.jmlspecs.samples.jmlrefman
Class RefineDemo2

java.lang.Object
  org.jmlspecs.samples.jmlrefman.RefineDemo2

public class RefineDemo2

extends Object

Class Specifications

protected represents x <- this.x_; public initially this.x == 0;

Specifications inherited from class Object

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

Model Field Summary
int	x

 

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
protected  int	x_

 

Constructor Summary
protected	RefineDemo2()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

x

public int x

Specifications:
datagroup contains: x_

x_

protected int x_

Specifications:
is in groups: x

RefineDemo2

protected RefineDemo2()

Specifications:

protected normal_behavior
assignable x;
ensures this.x == 0;