org.jmlspecs.checker
Class JmlParser.TypeWeaklyList

java.lang.Object
  org.jmlspecs.checker.JmlParser.TypeWeaklyList

Enclosing class:

JmlParser

static class JmlParser.TypeWeaklyList

extends Object

This nested class represents a list of implemented interfaces for a class declaration (or extends interfaces for an interface declaration) and whether they are implemented (or extended) weakly.

Field Summary
private  int[]	indices
private  int	indicesSize
private  ArrayList	types

 

Constructor Summary
(package private)	JmlParser.TypeWeaklyList()

 

Method Summary
(package private)  void	add(CClassType type, boolean _weakly)            model_program { weaklyFlags.add( new Boolean( _weakly ) ); } also assignable weaklyFlags;
private  void	growIndices()
(package private)  CClassType[]	types()
(package private)  boolean[]	weaklyFlags()            model_program { Boolean[] result = new Boolean[ weaklyFlags.size() ]; weaklyFlags.toArray( result ); boolean[] res = new boolean[ weaklyFlags.size() ]; normal_behavior assignable res; ensures (\forall int i; 0<=i && i < res.length; result[i].booleanValue() == res[i]); return res; }

 

Methods inherited from class java.lang.Object

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

 

Field Detail

types

private ArrayList types

indices

private int[] indices

indicesSize

private int indicesSize

JmlParser.TypeWeaklyList

JmlParser.TypeWeaklyList()

add

void add(CClassType type,
         boolean _weakly)

 model_program {
    weaklyFlags.add( new Boolean( _weakly ) );
 }
 also
 assignable weaklyFlags;
 

types

CClassType[] types()

weaklyFlags

boolean[] weaklyFlags()

 model_program {
    Boolean[] result = new Boolean[ weaklyFlags.size() ];
    weaklyFlags.toArray( result );
    boolean[] res = new boolean[ weaklyFlags.size() ];
    normal_behavior
      assignable res;
      ensures (\forall int i; 0<=i && i < res.length;
                    result[i].booleanValue() == res[i]);
    return res;
 }
 

growIndices

private void growIndices()