Go to the first, previous, next, last section, table of contents.

Concept Index

Jump to: ! - ( - * - + - - - . - / - ; - < - = - @ - \ - a - b - c - d - e - f - g - h - i - j - k - l - m - n - o - p - q - r - s - t - u - v - w - z - { - |

!

  • !=, for booleans

    • (

  • (*, (*

    • *

  • *), *)
  • *, in array range

    • +

  • ++, prohibited in assertions
  • +=, prohibited in assertions

    • -

  • --, prohibited in assertions
  • -=, prohibited in assertions
  • -R option to jml script

    • .

  • ..
  • `.java'
  • .java files
  • `.java-refined'
  • `.jml', `.jml'
  • `.jml-refined', `.jml-refined'
  • .jml-refined files
  • `.refines-java'
  • `.refines-jml'
  • `.refines-spec'
  • `.spec', `.spec'
  • `.spec-refined', `.spec-refined'

    • /

  • /*+@ vs. /*@ annotations
  • /*@
  • //
  • //+@ vs. //@ annotations
  • //@

    • ;

  • ;, in quantifiers

    • <

  • <
  • <-
  • </esc>
  • </jml>
  • </pre></esc>
  • </pre></jml>
  • <:
  • <=
  • <=!=>
  • <==
  • <==>, <==>
  • <esc>
  • <jml>
  • <pre><esc>
  • <pre><jml>

    • =

  • =, prohibited in assertions
  • ==, for booleans
  • ==, to compare values
  • ==, vs equals
  • ==, vs. equals
  • ==>

    • @

  • @*/
  • @, in annotations

    • \

  • \duration, \duration
  • \elemtype
  • \exists
  • \forall
  • \fresh
  • \into
  • \invariant_for
  • \is_initialized
  • \lblneg
  • \lblpos
  • \lockset
  • \max, \max
  • \min
  • \nonnullelements
  • \not_modified
  • \not_specified, \not_specified
  • \nothing
  • \num_of
  • \old, \old, \old
  • \old, pitfalls of
  • \old, semantics of, \old, semantics of
  • \product
  • \reach
  • \result, \result
  • \space
  • \such_that
  • \sum
  • \type
  • \typeof
  • \working_space, \working_space

    • a

  • abstract class
  • abstract data type, implementation of
  • abstract data types
  • abstract model
  • abstract model, adding to
  • abstract modeling classes
  • abstract models
  • abstraction function, see represents clause
  • abstraction relation, see represents clause
  • abstraction relations
  • acknowledgments
  • adding, to abstract model
  • adding, to method specification
  • adding, to supertype's model
  • addition, quantified see \sum
  • ADT, correctness of implementation
  • ADT, implementation of
  • ADT, modeling
  • ADT, specification of
  • allocation, vs. modification
  • also, also, also, also, also, also, also
  • Amtoft
  • annotations, annotations
  • annotations, in documentation comments
  • annotations, placement of
  • Arnold
  • array range
  • array ranges
  • array, specifying elements are non-null
  • assert
  • assertion checking
  • assertion, embedded
  • assertions, additions to Java expressions for
  • assertions, expressions in
  • assertions, in Java vs. JML
  • assertions, Java expressions prohibited in
  • assertions, semantics of
  • assign to, locations a method can
  • assignable, assignable, assignable, assignable, assignable, assignable
  • assignable clause, assignable clause, assignable clause
  • assignable clause, and constructors
  • assignable clause, and data groups
  • assignable clause, checks
  • assignable clause, redundancy in
  • assignable clause, semantics of
  • assignable clauses, and data groups
  • assignable, default for
  • assignable_redundantly
  • assignment
  • assignment, to model variables
  • assume

    • b

  • Büchi, Büchi
  • Back, Back, Back, Back
  • Baker, Baker
  • Becker
  • behavior
  • behavior, use in desugaring
  • behavior, when to use
  • behavior, vs. normal_behavior
  • behavioral interface specification language
  • behavioral subtyping
  • benevolent side effect
  • Bhorkar
  • BISL
  • blank final, and constructor specifications
  • body of a quantifier
  • Borgida
  • Boyland
  • breaks, default for

    • c

  • case analysis, nested
  • case analysis, nested, example of
  • Chalin
  • Chan, Judy
  • Chan, Peter, Chan, Peter
  • checkable redundancy
  • checker
  • checker, for JML
  • Cheon
  • Cheon, Yoonsik
  • class initialization predicate
  • class specification
  • classes, pure, use of
  • clauses, multiple
  • client, specification for
  • Clifton
  • clone, clone
  • Cohen, Cohen
  • Cok, Cok
  • collection model types
  • command for checking JML files
  • Compaq SRC, Compaq SRC
  • comprehensions, for sets
  • conclusions
  • concrete fields, relating to models
  • concurrency
  • constraint
  • constructor, and preconditions
  • constructor, pure
  • constructors, and the assignable clause
  • container classes, in JML models directory
  • continues, default for
  • contract
  • correct implementation
  • correctness
  • correctness, of ADT implementation
  • cycle, virtual machine

    • d

  • da Costa Gomez
  • Daikon invariant detector
  • data abstraction
  • data group
  • data group membership
  • data groups
  • data groups, and assignable clause
  • data groups, and assignable clauses
  • data groups, and frame axioms
  • data groups, and modifies clauses
  • data type induction
  • Daugherty
  • Davies
  • debugging, specifications
  • default privacy
  • default, for requires clause
  • defaults, for omitted clauses in method specifications
  • desugaring for spec_public and spec_protected
  • Dhara, Dhara
  • directory, argument to jml script
  • diverges
  • diverges, default for
  • documentation comment, specification in
  • Docxx
  • Dooren
  • downloading, JML
  • duration, default for
  • duration, specification of
  • dynamic type of an expression
  • dynamic, assertion checking

    • e

  • Edwards
  • Eiffel, Eiffel, Eiffel, Eiffel, Eiffel
  • element type, see \elemtype
  • empty range
  • ensures, ensures
  • ensures clause, meaning of multiple
  • ensures, default for
  • ensures, multiple
  • ensures_redundantly
  • equality, guidelines for comparing
  • equals, equals
  • equals, vs. ==, equals, vs. ==
  • equivalence, see <==>
  • Ernst, Ernst
  • error, in Java virtual machine
  • ESC/Java, ESC/Java, ESC/Java, ESC/Java, ESC/Java, ESC/Java
  • ESC/Java, goals
  • example
  • examples, checking
  • examples, in method specifications
  • exceptional_behavior, exceptional_behavior
  • exceptional_behavior, desugaring
  • exceptional_example
  • exceptions, in expressions
  • exceptions, prohibiting others
  • exceptions, semantics of signals clauses
  • exceptions, specification of, exceptions, specification of
  • exceptions, specifying details of
  • existential quantifier, see \exists
  • expressions, additions to Java
  • expressions, in assertions
  • exsures, see signals

    • f

  • fields of an object
  • fields, of an ADT
  • filename suffixes
  • files, for annotations
  • finiteness constraints
  • Finney
  • Fitzgerald
  • Fleck
  • for_example
  • formal parameters, and assignable clause
  • formality, escape from
  • frame axiom
  • frame axiom, see assignable clause
  • frame axioms, and data groups
  • fresh predicate
  • future work

    • g

  • Ganapathy, Ganapathy
  • generalized quantifier
  • Gifford
  • goals, of JML, goals, of JML
  • Gosling
  • Gries
  • Guttag, Guttag

    • h

  • Hayes
  • heavyweight specification
  • heavyweight specifications
  • helper
  • hiding concrete fields, in specifications
  • history constraint
  • history constraint, example of
  • Hoare, Hoare, Hoare, Hoare
  • Hoech
  • Holmes, Holmes
  • Horning, Horning
  • HTML documentation
  • Huisman, Huisman
  • hypertext, generation from JML specifications

    • i

  • if
  • if and only if, see <==>
  • iff, see <==>
  • immutable types, defining your own
  • implementation, correctness of
  • implication
  • implication, see ==>
  • implications section, of method specification
  • implications, of a specification
  • implies_that
  • implies_that, example of
  • in, in
  • in clause
  • in, example of
  • inequivalence, see <=!=>
  • informal descriptions
  • informal predicate, example of
  • informal predicates
  • informality
  • information hiding
  • inheritance
  • inheritance, of instance fields
  • inheritance, of method specifications
  • inheritance, of specifications
  • initialization, in constructors
  • initialization, specification that a class is
  • initially
  • instance, instance
  • instance, history constraint
  • instance, invariant
  • interface specification, interface specification
  • interface, of a module
  • invariant, invariant
  • invariant checking
  • invariant, example of
  • invariant, for an object
  • invariant, redundant
  • invariant_redundantly
  • Iowa State University, Com S 362
  • Iowa State, release of JML
  • Iowa, University of
  • isAssignableFrom, method of java.lang.Class
  • ISO
  • ISU, Com S 362

    • j

  • Jacobs, Jacobs
  • Java
  • `java' filename suffix
  • Java Modeling Language
  • Java vs. JML assertions
  • Java, additions to expressions
  • Java, expressions prohibited in assertions
  • Java, failures in virtual machine
  • `java-refined' filename suffix
  • java.lang.Class, vs. \type()
  • javadoc
  • javadoc comments
  • JML, JML
  • JML checker, JML checker
  • `jml' filename suffix
  • jml script
  • JML vs. Java assertions
  • JML, downloading
  • JML, web page
  • jml-junit script
  • `jml-refined' filename suffix
  • jmlc script
  • jmldoc script
  • JMLObjectSet
  • jmlrac script
  • jmlunit script
  • JMLValueSet, JMLValueSet
  • Jones, Jones
  • Jonkers
  • Jouvelot
  • jtest script
  • JUnit

    • k

  • Kiniry

    • l

  • label (negative)
  • label (positive)
  • Larch, Larch
  • Larch, differences from
  • Larch/C++, Larch/C++
  • Larsen
  • Lea
  • Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens, Leavens
  • Leino, Leino, Leino, Leino, Leino, Leino, Leino, Leino, Leino
  • Lerner
  • lightweight specification
  • lightweight specifications, lightweight specifications
  • Liskov
  • local variables, and assignable clause
  • locking order
  • locking order, max
  • locks held by a thread
  • logic, undefinedness in
  • logical equivalence, see <==>
  • logical implication, see ==>
  • Loop
  • Lucassen
  • Luckham

    • m

  • Müller, Müller
  • maps, maps
  • maps-into clause
  • mathematical modeling
  • max of objects in locking order
  • maximum, see \max
  • measured_by
  • measured_by, default for
  • Mertens
  • method call, space used by
  • method specification, method specification
  • method specification, addition to
  • method specification, multiple clauses in
  • method specification, omitted
  • method specifications, defaults for clauses
  • method, pure
  • method, result of
  • Meyer, Meyer, Meyer
  • Mikhajlova
  • Millstein
  • minimum, see \min
  • MIT
  • model
  • model class, example of
  • model classes, model classes
  • model classes, vs. pure classes
  • model declaration
  • model field
  • model fields, from spec_protected
  • model fields, from spec_public
  • model fields, in interfaces
  • model fields, inheritance of
  • model fields, relating to concrete
  • model import
  • model method, example of, model method, example of
  • model methods, vs. pure methods
  • model types
  • model types, for collections
  • model types, value vs. object
  • model variables, modification of
  • model, for a subtype
  • model-based specification
  • modeling types, defining your own
  • modeling, for ADTs, example of
  • modifiable, see assignable
  • modification, of model variables
  • modification, specifying its opposite
  • modified
  • modifies clause
  • modifies clauses, and data groups
  • modifies, see assignable
  • modify, locations a method can
  • module
  • monitors
  • Morgan, Morgan, Morgan, Morgan
  • multiple clauses
  • multiple specification cases
  • multiple, exceptions
  • multiplication, quantified, see \product
  • Mylopoulos

    • n

  • Namara, Namara
  • new, new
  • new {|}
  • new, and assertions
  • Nielson
  • Nijmegen, University of, Nijmegen, University of
  • non-null
  • non-null elements, of an array
  • nondeterminism in exception specifications
  • normal termination
  • normal_behavior, normal_behavior
  • normal_behavior, desugaring
  • normal_example
  • NSF
  • null, protection from
  • numerical quantifier, see \num_of

    • o

  • Ogden
  • old
  • old values, old values
  • old values, semantics of
  • Oltes
  • omitted clauses in method specifications
  • omitted privacy in specification
  • omitted specification, meaning of
  • omitted, assignable clause
  • org.jmlspecs.models package, org.jmlspecs.models package
  • overriding, and method specifications
  • overriding, specification of

    • p

  • partiality
  • pitfalls, in specifying exceptions
  • Poetzsch-Heffter, Poetzsch-Heffter, Poetzsch-Heffter
  • Poll
  • Poll, Erik
  • post-state
  • post, see ensures
  • postcondition
  • postcondition checking
  • postcondition, multiple
  • Potts
  • pre-state
  • pre, see requires
  • precondition
  • precondition checking
  • preconditions, and constructors
  • predicates, additions to Java expressions for
  • predicates, Java expressions prohibited in
  • private
  • product, see \product
  • protection, from undefinedness
  • protection, in method specification
  • protection, of precondition
  • prototyping from specifications
  • public specification
  • public, omitted
  • publicly visible state
  • pure
  • pure classes, use in modeling
  • pure classes, vs. model classes
  • pure constructor
  • pure interface
  • pure method, pure method
  • pure methods, vs. model methods
  • pure model class, example of
  • pure model method, example of
  • pure, example of
  • purity

    • q

  • quantified addition, see \sum
  • quantified maximum, see \max
  • quantified minimum, see \min
  • quantified multiplication, see \product
  • quantifier, body
  • quantifier, generalized
  • quantifier, range predicate in
  • quantifiers, quantifiers

    • r

  • Raghavan, Raghavan, Raghavan, Raghavan
  • range predicate, in quantifier
  • range predicate, not satisfiable
  • reachable objects
  • recursion
  • recursion, in model methods
  • redundancy, redundancy
  • redundancy, checking
  • redundancy, in assignable clause
  • redundant examples
  • redundant, ensures clauses
  • redundantly, suffix on keywords
  • reference semantics, and \old
  • reference semantics, and equality
  • reference types
  • reference types, and equality tests
  • refine, refine
  • refinement
  • refinement calculus, refinement calculus
  • `refines-java' filename suffix
  • `refines-jml' filename suffix
  • `refines-spec' filename suffix
  • reflection in assertions
  • Reiter
  • release, of JML
  • represents
  • represents clause, represents clause, represents clause
  • represents clause, and reasoning
  • represents, example of
  • requires, requires, requires
  • requires clauses, and constructors
  • requires, default for
  • RESOLVE
  • resources, specification of, resources, specification of, resources, specification of
  • result, of a method
  • returns, default for
  • reverse implication, see <==
  • rhetorical points
  • Rockwell International Corporation
  • Rosenblum
  • Ruby
  • run-time assertion checking
  • runtime assertion checking
  • Russell
  • Russell's paradox

    • s

  • Salcianu
  • Sather
  • Sather-K
  • satisfaction, see correct implementation
  • Saxe
  • Scherbring
  • Schneider
  • semantics of signals clauses
  • set comprehension
  • Shilling
  • side effects, freedom from in assertions
  • side-effects
  • signals, signals, signals
  • signals clause
  • signals clauses, detailed
  • signals, default for
  • simultaneous exceptions
  • Sivaprasad
  • space, specification of
  • space, taken up by an object
  • `spec' filename suffix
  • `spec-refined' filename suffix
  • spec_protected
  • spec_protected, as a model field shorthand
  • spec_public
  • spec_public, as a model field shorthand
  • specification case, nested
  • specification cases
  • specification cases, multiple
  • specification of examples
  • specification of exceptions, specification of exceptions
  • specification, of methods
  • specification, of overriding method
  • specification, of subtypes
  • specification-only declaration
  • Spivey
  • Stata
  • static, history constraint
  • static, invariant
  • store-references, additions to Java for
  • subtype, subtype
  • subtype relation
  • subtype, adding to supertype's model
  • subtype, specification
  • subtyping
  • suffixes, of filenames
  • summation, see \sum
  • super, prohibited in assertions
  • supertype
  • supertype, specification of

    • t

  • Talpin
  • Tan, Tan
  • Tan, Roy
  • temporary side effects
  • termination function, for methods
  • termination, normal
  • test data
  • test oracle
  • textual copying, and inheritance
  • Thomas
  • thread, specifying locks held by
  • time, specification of
  • time, virtual machine cycle
  • tool support, for JML
  • type checking, of specifications
  • type, correctness of implementation
  • typeof operator
  • types for mathematical modeling
  • types, comparing
  • types, marking in expressions

    • u

  • undefinedness, in expressions
  • undefinedness, protection from, undefinedness, protection from
  • unit testing, with JML
  • universal quantifier, see \forall
  • University of Iowa, 22C:181
  • University of Nijmegen, University of Nijmegen
  • unmodified, see \not_modified
  • URL, for JML

    • v

  • value, vs. object model types
  • van den Berg
  • VDM-SL
  • Vickers, Vickers, Vickers
  • virtual machine cycle time
  • von Henke
  • von Wright, von Wright, von Wright, von Wright

    • w

  • Wahls, Wahls
  • web page, for JML
  • Weck, Weck
  • when
  • when, default for
  • Whitehead
  • Wills
  • Wing, Wing, Wing, Wing, Wing, Wing, Wing, Wing, Wing, Wing
  • Woodcock
  • working space, specification of
  • working_space, default for
  • Wright

    • z

  • Z, specification language
  • Zhou

    • {

  • {|, {|
  • {|}

    • |

  • |}, |}

    • Go to the first, previous, next, last section, table of contents.