org.jmlspecs.samples.jmlrefman
Class RefineDemo

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

public class RefineDemo

extends Object

Class Specifications

protected represents x <- this.x_;

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

RefineDemo()

 

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

RefineDemo

public RefineDemo()

Specifications:

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