[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

Index: H -- I

Jump to:   !   "   $   %   &   '   (   )   *   +   ,   -   .   /   0   1   2   3   4   5   6   7   8   9   :   ;   <   =   >   ?   @   [   \   ]   ^   _   {   |   }   ~  
A   B   C   D   E   F   G   H   I   J   K   L   M   N   O   P   Q   R   S   T   U   V   W   Z  

Index Entry Section

H
Hall1.3 What is JML Good For?
handbook, for LSL1.5 Historical Precedents
Handbook, for LSL1.5 Historical Precedents
handler, defined13. Statements and Annotation Statements
has12.5 Set Comprehensions
Hayes1.1 Behavioral Interface Specifications
Hayes1.5 Historical Precedents
HeavyweightSemantics
heavyweight example14.2 Redundant Examples
heavyweight specification1.2 A First Example
heavyweight specification2.3 Lightweight and Heavyweight Specifications
heavyweight specification case9.5 Heavyweight Specification Cases
heavyweight specification, vs. lightweight1.2 A First Example
heavyweight-spec-case, defined9.5 Heavyweight Specification Cases
heavyweight-spec-case, used9.2 Organization of Method Specifications
helper4.6 Tokens
helper6.2 Modifiers
helper6.2.9 Helper
helper7.1.1.4 Helper Methods and Constructors
helper8.2 Invariants
helper8.2 Invariants
helper constructor, and invariants8.2 Invariants
helper method, and invariants8.2 Invariants
helper, and invariants6.2.9 Helper
helper, and private6.2.9 Helper
hence-by-keyword, defined13.4.6 Hence By Statements
hence-by-keyword, used13.4.6 Hence By Statements
hence-by-statement, defined13.4.6 Hence By Statements
hence-by-statement, used13.4 JML Annotation Statements
hence_by4.6 Tokens
hence_by13.4.6 Hence By Statements
hence_by_redundantly4.6 Tokens
hence_by_redundantly13.4.6 Hence By Statements
hex-digit, defined4.6 Tokens
hex-digit, used4.6 Tokens
hex-integer-literal, defined4.6 Tokens
hex-integer-literal, used4.6 Tokens
hex-numeral, defined4.6 Tokens
hex-numeral, used4.6 Tokens
higher-order method specification15.1 Ideas Behind Model Programs
history constraint6.1.1 Subtyping for Type Declarations
history constraint11. Specification Inheritance
history constraints, vs. helper6.2.9 Helper
history-constraint, defined8.3 Constraints
history-constraint, used8. Type Specifications
Hoare1.5 Historical Precedents
Hoare1.5 Historical Precedents
Hoare2.2 Model and Ghost
Holmes1. Introduction
Horning1.1 Behavioral Interface Specifications
Horning1.3 What is JML Good For?
Horning1.5 Historical Precedents
Horning1.5 Historical Precedents
Huisman1.3 What is JML Good For?
Huisman1.3 What is JML Good For?
Hussain, Faraz1.6 Acknowledgments

I
ident, defined4.6 Tokens
ident, used4. Lexical Conventions
ident, used5.1 Package Declarations
ident, used5.2 Import Declarations
ident, used6.1 Class and Interface Declarations
ident, used6.2.2 Java Annotations
ident, used7.1.1 Method and Constructor Declarations
ident, used7.1.1.1 Formal Parameters
ident, used7.1.2 Field and Variable Declarations
ident, used8.3 Constraints
ident, used8.7 Readable If Clauses
ident, used8.8 Writable If Clauses
ident, used8.9 Monitors For Clause
ident, used9.9.4 Signals Clauses
ident, used10.1 Static Data Group Inclusions
ident, used10.2 Dynamic Data Group Mappings
ident, used12.3 Expressions
ident, used12.4.2 \old and \pre
ident, used12.4.23 \lblneg and \lblpos
ident, used12.4.24 Quantified Expressions
ident, used12.5 Set Comprehensions
ident, used12.7 Store Refs
ident, used13. Statements and Annotation Statements
ident, used13.2 Loop Statements
ident, used13.2 Loop Statements
ident, used15.6.1 Continues Clause
identifiers4.6 Tokens
if4.6 Tokens
if8.7 Readable If Clauses
if8.8 Writable If Clauses
if9.9.12 Measured By Clauses
if9.9.14 Working Space Clauses
if9.9.15 Duration Clauses
if13. Statements and Annotation Statements
ignored-at-in-annotation, defined4.4 Annotation Markers
ignored-at-in-annotation, used4.4 Annotation Markers
immutable6.1.2.1 Pure Type Declarations
immutable, vs. pure6.1.2.1 Pure Type Declarations
implementation of interfaces6.1.1 Subtyping for Type Declarations
implements4.6 Tokens
implements6.1.1 Subtyping for Type Declarations
implements, for classes6.1.1 Subtyping for Type Declarations
implements-clause, defined6.1.1 Subtyping for Type Declarations
implements-clause, used6.1 Class and Interface Declarations
implements-clause, used6.1.1 Subtyping for Type Declarations
implication, redundant14.1 Redundant Implications and Redundantly Clauses
implication, see ==>12.6.3 Forward and Reverse Implication Operators
implications, defined14.1 Redundant Implications and Redundantly Clauses
implications, used14. Redundancy
implicitly nullable6.2.13 Nullity Modifiers
ImplicitOld9.9.6 Parameters in Postconditions
implies-expr, defined12.3 Expressions
implies-expr, used12.3 Expressions
implies-non-backward-expr, defined12.3 Expressions
implies-non-backward-expr, used12.3 Expressions
implies_that4.6 Tokens
implies_that14.1 Redundant Implications and Redundantly Clauses
import4.6 Tokens
import5.2 Import Declarations
import declaration5.2 Import Declarations
import, model5.2 Import Declarations
import-declaration, defined5.2 Import Declarations
import-declaration, used5. Compilation Units
in4.6 Tokens
in10.1 Static Data Group Inclusions
in-group-clause, defined10.1 Static Data Group Inclusions
in-group-clause, used10. Data Groups
in-keyword, defined10.1 Static Data Group Inclusions
in-keyword, used10.1 Static Data Group Inclusions
in_redundantly4.6 Tokens
in_redundantly10.1 Static Data Group Inclusions
inclusive-or-expr, defined12.3 Expressions
inclusive-or-expr, used12.3 Expressions
incompatible changesB. Incompatible Changes
InconsistentMethodSpec9.8.1 Pragmatics of Exceptional Behavior Specifications Cases
InconsistentMethodSpec29.8.1 Pragmatics of Exceptional Behavior Specifications Cases
infinite precision numeric types19. Safe Math Extensions
influences, on JML evolution1.4 Status and Plans for JML
informal descriptions4.6 Tokens
informal-description, defined4.6 Tokens
informal-description, used4. Lexical Conventions
informal-description, used12.4 JML Primary Expressions
informal-description, used12.7 Store Refs
information hiding, in assignable clauses10. Data Groups
inheritance6.1.1 Subtyping for Type Declarations
inheritance6.1.1 Subtyping for Type Declarations
inheritance, multiple6.1.1 Subtyping for Type Declarations
inheritance, of JML features6.1.1 Subtyping for Type Declarations
inheritance, of JML features6.1.1 Subtyping for Type Declarations
inheritance, of JML features11. Specification Inheritance
inheritance, of model methods from interfaces6.1.1 Subtyping for Type Declarations
inheritance, of specifications6.1.1 Subtyping for Type Declarations
inheritance, of specifications6.1.1 Subtyping for Type Declarations
inheritance, of specifications11. Specification Inheritance
inherits6.1.1 Subtyping for Type Declarations
initialization, specification that a class is12.4.21 \is_initialized
initializer4.6 Tokens
initializer, defined7.1.2 Field and Variable Declarations
initializer, defined12.3 Expressions
initializer, separate files17.3 Type Checking Separate Files
initializer, used7.1.2 Field and Variable Declarations
initializer, used7.2 Class Initializer Declarations
initializer, used12.3 Expressions
initializer-list, defined7.1.2 Field and Variable Declarations
initializer-list, used7.1.2 Field and Variable Declarations
initializers, for fields field17.3 Type Checking Separate Files
initializers, separate files17.3 Type Checking Separate Files
initially4.6 Tokens
initially8.5 Initially Clauses
initially, clause and separate files17.3 Type Checking Separate Files
initially-clause, defined8.5 Initially Clauses
initially-clause, used8. Type Specifications
instance2.5 Instance vs. Static
instance4.6 Tokens
instance6.2 Modifiers
instance6.2.8 Instance
instance7.1.2.1 JML Modifiers for Fields
instance8.2.1 Static vs. instance invariants
instance8.3.1 Static vs. instance constraints
instance constraint8.3.1 Static vs. instance constraints
instance features2.5 Instance vs. Static
instance invariant8.2 Invariants
instance invariant8.2.1 Static vs. instance invariants
instance invariant8.2.1 Static vs. instance invariants
instance vs. final, in interfaces7.1.2.1 JML Modifiers for Fields
instance vs. static7.1.2.1 JML Modifiers for Fields
instanceof4.6 Tokens
instanceof12.3 Expressions
instanceof, and ownership types18.7 Casts and Ownership Types
instanceof, default ownership modifiers for18.5 Default Ownership Modifiers
instanceof, default ownership modifiers for types in18.5 Default Ownership Modifiers
int4.6 Tokens
int12.3 Expressions
integer-literal, defined4.6 Tokens
integer-literal, used4.6 Tokens
integer-type-suffix, defined4.6 Tokens
integer-type-suffix, used4.6 Tokens
interface4.6 Tokens
interface6.1 Class and Interface Declarations
interface declaration6.1 Class and Interface Declarations
interface declarations6. Type Declarations
interface specification1.1 Behavioral Interface Specifications
interface, field1.1 Behavioral Interface Specifications
interface, method1.1 Behavioral Interface Specifications
interface, modifiers for declarations of6.1.2 Modifiers for Type Declarations
interface, type1.1 Behavioral Interface Specifications
interface-declaration, defined6.1 Class and Interface Declarations
interface-declaration, defined6.1.1 Subtyping for Type Declarations
interface-declaration, used6. Type Declarations
interface-declaration, used7.1 Java Member Declarations
interface-extends, defined6.1.1 Subtyping for Type Declarations
interface-extends, used6.1 Class and Interface Declarations
interfaces, and default modifier for fields6.2.6 Model
interfaces, and default modifier for fields6.2.7 Ghost
interfaces, and ghost fields6.2.7 Ghost
interfaces, and model fields6.2.6 Model
IntHeap1.2 A First Example
Invariant8.2 Invariants
invariant4.6 Tokens
invariant8.2 Invariants
invariant, and helper constructors7.1.1.4 Helper Methods and Constructors
invariant, and helper methods7.1.1.4 Helper Methods and Constructors
invariant, assuming8.2 Invariants
invariant, defined8.2 Invariants
invariant, enforcement8.2 Invariants
invariant, establishing8.2 Invariants
invariant, for an object12.4.22 \invariant_for
invariant, instance8.2 Invariants
invariant, instance vs. static8.2.1 Static vs. instance invariants
invariant, preserving8.2 Invariants
invariant, reasoning about8.2 Invariants
invariant, static8.2 Invariants
invariant, static vs. instance8.2.1 Static vs. instance invariants
invariant, used8. Type Specifications
invariant, used15.3 Details of Model Programs
invariant-for-expression, defined12.4.22 \invariant_for
invariant-for-expression, used12.4 JML Primary Expressions
invariant-keyword, defined8.2 Invariants
invariant-keyword, used8.2 Invariants
invariant_redundantly4.6 Tokens
invariant_redundantly8.2 Invariants
invariants, and modularity8.2 Invariants
invariants, vs. helper6.2.9 Helper
is-initialized-expression, defined12.4.21 \is_initialized
is-initialized-expression, used12.4 JML Primary Expressions
isAssignableFrom, method of java.lang.Class12.6.1 Subtype operator
ISO1.5 Historical Precedents

Jump to:   !   "   $   %   &   '   (   )   *   +   ,   -   .   /   0   1   2   3   4   5   6   7   8   9   :   ;   <   =   >   ?   @   [   \   ]   ^   _   {   |   }   ~  
A   B   C   D   E   F   G   H   I   J   K   L   M   N   O   P   Q   R   S   T   U   V   W   Z  


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html