JML

org.jmlspecs.checker
Class JmlParser.TypeWeaklyList

java.lang.Object
  extended byorg.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
Constructor Detail

JmlParser.TypeWeaklyList

JmlParser.TypeWeaklyList()
Method Detail

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()

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.