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

Index: J -- L

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

J
Jackson16.2 Code Contracts
Jacobs1.3 What is JML Good For?
Jacobs1.3 What is JML Good For?
Jacobs1.6 Acknowledgments
Java1. Introduction
Java annotation6.2.2 Java Annotations
`java' filename suffix17.1 File Name Suffixes
Java modifiers6.2 Modifiers
Java reserved words4.6 Tokens
Java virtual machine error, and method semantics9.6.2 Semantics of non-helper methods
Java vs. JML-only names, resolving conflicts2.2 Model and Ghost
java-annotation, defined6.2.2 Java Annotations
java-annotation, used6.2 Modifiers
java-annotation, used6.2.2 Java Annotations
java-annotations, defined6.2.2 Java Annotations
java-annotations, used5.1 Package Declarations
java-literal, defined4.6 Tokens
java-literal, used4. Lexical Conventions
java-literal, used12.3 Expressions
java-operator, defined4.6 Tokens
java-operator, used4.6 Tokens
java-reserved-word, defined4.6 Tokens
java-reserved-word, used4.6 Tokens
java-separator, defined4.6 Tokens
java-separator, used4.6 Tokens
java-special-symbol, defined4.6 Tokens
java-special-symbol, used4.6 Tokens
java-universe-reserved, defined4.6 Tokens
java.lang.Class, and \TYPE7.1.2.2 Type-Specs
java.lang.Class, vs. \type()12.4.18 \type
javadoc4.5 Documentation Comments
JML annotation4.4 Annotation Markers
`jml' filename suffix17.1 File Name Suffixes
JML keywords, where recognized4.6 Tokens
JML status and plans1.4 Status and Plans for JML
JML web site1. Introduction
JML, evolution1.4 Status and Plans for JML
JML, plans1.4 Status and Plans for JML
JML, status1.4 Status and Plans for JML
jml-annotation-statement, defined13.4 JML Annotation Statements
jml-annotation-statement, used13. Statements and Annotation Statements
jml-annotation-statement, used13. Statements and Annotation Statements
jml-compound-statement, defined15.3 Details of Model Programs
jml-compound-statement, used15.3 Details of Model Programs
jml-compound-statement, used15.4 Nondeterministic Choice Statement
jml-compound-statement, used15.5 Nondeterministic If Statement
jml-data-group-clause, defined10. Data Groups
jml-data-group-clause, used7.1.2 Field and Variable Declarations
jml-data-group-clause, used7.1.2 Field and Variable Declarations
jml-declaration, defined8. Type Specifications
jml-declaration, used7. Class and Interface Member Declarations
jml-keyword, defined4.6 Tokens
jml-keyword, used4.6 Tokens
jml-modifier, defined6.2 Modifiers
jml-modifier, used6.2 Modifiers
JML-only vs. Java names, resolving conflicts2.2 Model and Ghost
jml-predicate-keyword, defined4.6 Tokens
jml-predicate-keyword, used4.6 Tokens
jml-primary, defined12.4 JML Primary Expressions
jml-primary, used12.3 Expressions
jml-special-symbol, defined4.6 Tokens
jml-special-symbol, used4.6 Tokens
jml-specs, defined4.5 Documentation Comments
jml-specs, used4.5 Documentation Comments
jml-statement, defined15.3 Details of Model Programs
jml-statement, used15.5 Nondeterministic If Statement
jml-tag, defined4.5 Documentation Comments
jml-tag, used4.5 Documentation Comments
jml-universe-keyword, defined4.6 Tokens
jml-universe-keyword, used4.6 Tokens
jml-universe-pkeyword, defined4.6 Tokens
jml-universe-pkeyword, used4.6 Tokens
jmlc1.3 What is JML Good For?
jmlc12.4.24.4 Executability of Quantified Expressions
jmlc, warnings for non-executable assertions12.4.24.4 Executability of Quantified Expressions
jmldoc1.3 What is JML Good For?
Jones1.5 Historical Precedents
Joy4.6 Tokens
Joy4.6 Tokens

K
key, negative4.4 Annotation Markers
key, positive4.4 Annotation Markers
keys, for conditional annotation, syntax4.4 Annotation Markers
keyword, defined4.6 Tokens
keyword, used4. Lexical Conventions
keywords4.6 Tokens
Khurshid16.2 Code Contracts
Kiczales16. Specification for Subtypes
KiniryG.1 Differences Between JML and Other Tools

L
L4.6 Tokens
l4.6 Tokens
label expression (negative)12.4.23 \lblneg and \lblpos
label expression (positive)12.4.23 \lblneg and \lblpos
Lamping16. Specification for Subtypes
Lamport1.1 Behavioral Interface Specifications
language level 0 features2.9.1 Level 0 Features
language level 1 features2.9.2 Level 1 Features
language level 2 features2.9.3 Level 2 Features
language level 3 features2.9.4 Level 3 Features
language level C features2.9.5 Level C Features
language level X features2.9.6 Level X Features
language levels2.9 Language Levels
language levels, and learning JML2.9 Language Levels
language levels, and tools2.9 Language Levels
Larch1.1 Behavioral Interface Specifications
Larch1.5 Historical Precedents
Larch Shared Language (LSL)1.1 Behavioral Interface Specifications
Larch style specification language1.1 Behavioral Interface Specifications
Larch/C++1.5 Historical Precedents
Larsen1.5 Historical Precedents
lblneg-expression, defined12.4.23 \lblneg and \lblpos
lblneg-expression, used12.4 JML Primary Expressions
lblpos-expression, defined12.4.23 \lblneg and \lblpos
lblpos-expression, used12.4 JML Primary Expressions
learning JML, and language levels2.9 Language Levels
Leavens1. Introduction
Leavens1.1 Behavioral Interface Specifications
Leavens1.2 A First Example
Leavens1.3 What is JML Good For?
Leavens1.3 What is JML Good For?
Leavens1.3 What is JML Good For?
Leavens1.5 Historical Precedents
Leavens2.4 Privacy Modifiers and Visibility
Leavens2.4 Privacy Modifiers and Visibility
Leavens2.7 Expression Evaluation and Undefinedness
Leavens2.7 Expression Evaluation and Undefinedness
Leavens6.1.1 Subtyping for Type Declarations
Leavens6.2.9 Helper
Leavens7.1.1.3 Pure Methods and Constructors
Leavens8.2 Invariants
Leavens11. Specification Inheritance
Leavens11. Specification Inheritance
Leavens14. Redundancy
Leavens14.1 Redundant Implications and Redundantly Clauses
Leavens14.2 Redundant Examples
Leavens15.1 Ideas Behind Model Programs
Leavens15.1 Ideas Behind Model Programs
Leavens16. Specification for Subtypes
Leavens16. Specification for Subtypes
Leavens16.2 Code Contracts
Leavens18.1 Basic Concepts of Universes
Ledgard3. Syntax Notation
Leino1.1 Behavioral Interface Specifications
Leino1.3 What is JML Good For?
Leino1.6 Acknowledgments
Leino2.2 Model and Ghost
Leino2.4 Privacy Modifiers and Visibility
Leino4.4 Annotation Markers
Leino6.2.10 Monitored
Leino6.2.11 Uninitialized
Leino7.1.2.1 JML Modifiers for Fields
Leino12.4.19 \lockset
LeinoG.1 Differences Between JML and Other Tools
letter, defined4.6 Tokens
letter, used4.2 Lexical Pragmas
letter, used4.5 Documentation Comments
letter, used4.6 Tokens
letter-or-digit, defined4.6 Tokens
letter-or-digit, used4.6 Tokens
level 0, JML features2.9 Language Levels
level 0, JML features2.9.1 Level 0 Features
level 1, JML features2.9 Language Levels
level 1, JML features2.9.2 Level 1 Features
level 2, JML features2.9 Language Levels
level 2, JML features2.9.3 Level 2 Features
level 3, JML features2.9 Language Levels
level 3, JML features2.9.4 Level 3 Features
level C, JML features2.9 Language Levels
level C, JML features2.9.5 Level C Features
level X, JML features2.9 Language Levels
level X, JML features2.9.6 Level X Features
levels, of language support2.9 Language Levels
lexeme, defined4. Lexical Conventions
lexeme, used4. Lexical Conventions
lexical conventions4. Lexical Conventions
lexical-pragma, defined4.2 Lexical Pragmas
lexical-pragma, used4. Lexical Conventions
LightweightSemantics
lightweight example14.2 Redundant Examples
lightweight specification2.3 Lightweight and Heavyweight Specifications
lightweight specification case9.4 Lightweight Specification Cases
lightweight specification, example of1.2 A First Example
lightweight specification, vs. heavyweight1.2 A First Example
lightweight specifications and access control2.4 Privacy Modifiers and Visibility
lightweight-spec-case, definedSyntax
lightweight-spec-case, used9.2 Organization of Method Specifications
Liskov1.2 A First Example
Liskov1.5 Historical Precedents
list vs. sequence, in grammar3. Syntax Notation
literals4.6 Tokens
local-declaration, defined13.1 Local Declaration Statements
local-declaration, used13. Statements and Annotation Statements
local-declaration, used13.2 Loop Statements
local-modifier, defined13.1.1 Modifiers for Local Declarations
local-modifier, used13.1.1 Modifiers for Local Declarations
local-modifiers, defined13.1.1 Modifiers for Local Declarations
local-modifiers, used13.1 Local Declaration Statements
location1.2 A First Example
location2.6 Locations and Aliasing
location10. Data Groups
locking order12.6.4 Lockset Ordering
locks held by a thread12.4.19 \lockset
lockset-expression, defined12.4.19 \lockset
lockset-expression, used12.4 JML Primary Expressions
logic, three-valued2.7 Expression Evaluation and Undefinedness
logic, two-valued2.7 Expression Evaluation and Undefinedness
logical implication, see ==>12.6.3 Forward and Reverse Implication Operators
logical rules, valid in JML2.7 Expression Evaluation and Undefinedness
logical-and-expr, defined12.3 Expressions
logical-and-expr, used12.3 Expressions
logical-or-expr, defined12.3 Expressions
logical-or-expr, used12.3 Expressions
long4.6 Tokens
long12.3 Expressions
LOOP1.3 What is JML Good For?
loop, exiting via break13.2.1 Loop Invariants
loop-invariant, defined13.2.1 Loop Invariants
loop-invariant, used13.2 Loop Statements
loop-stmt, defined13.2 Loop Statements
loop_invariant4.6 Tokens
loop_invariant13.2.1 Loop Invariants
loop_invariant_redundantly4.6 Tokens
loop_invariant_redundantly13.2.1 Loop Invariants
LSL1.1 Behavioral Interface Specifications
LSL Handbook1.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