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


Concept Index

!

  • !, !, !
  • !=, !=, !=
  • "

  • ", ", "
  • #

  • #, #
  • #include
  • $

  • $
  • %

  • %
  • %)
  • %=
  • %>
  • &

  • &, &, &, &, &
  • &&, &&
  • &=
  • '

  • ', ', ', '
  • (

  • (, (, (, (, (, (, (, (, (
  • (%
  • (), ()
  • )

  • ), ), ), ), ), ), ), ), )
  • *

  • *, *, *, *, *, *, *, *
  • * in modifies clause
  • */
  • *=
  • +

  • +, +, +
  • ++
  • +=
  • ,

  • ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,, ,
  • -

  • -, -, -
  • --
  • -=
  • ->, ->
  • ->*
  • -list suffix
  • -seq suffix
  • .

  • ., .
  • ..., ...
  • ...
  • /

  • /, /
  • /*
  • /* */
  • /*@
  • //
  • //, //, //
  • //@
  • /=
  • /\
  • :

  • :, :, :, :, :, :, :, :
  • ::, ::, ::, ::, ::
  • ::*, ::*
  • :>
  • ;

  • ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;, ;
  • <

  • <, <, <, <
  • <%
  • <:
  • <<
  • <<, friendship grant for
  • <<=
  • <=
  • =

  • =, =, =, =, =, =, =, =
  • ==, ==, ==
  • =>
  • >

  • >, >, >, >
  • >=
  • >>
  • >>, friendship grant for
  • >>=
  • ?

  • ?
  • @

  • @, @
  • @*/
  • [

  • [, [, [
  • []
  • [], [], [], []
  • \

  • \, \
  • \"
  • \'
  • \, as start of lsl-op
  • \/
  • \<, \<
  • \<\>
  • \?
  • \\
  • \a
  • \A, \A
  • \and, \and
  • \any, \any
  • \b
  • \E, \E
  • \eq, \eq
  • \exists, \exists
  • \f
  • \forall, \forall
  • \ident{}, removed form
  • \implies
  • \langle, \langle
  • \n
  • \neq, \neq
  • \obj, \obj
  • \or
  • \post, \post
  • \pre, \pre
  • \r
  • \rangle, \rangle
  • \t
  • \v
  • ]

  • ], ], ]
  • ^

  • ^, ^
  • ^=
  • _

  • __attribute__
  • `

  • `'
  • a

  • A
  • abstract, abstract, abstract
  • abstract character string
  • abstract class
  • abstract data type
  • abstract program
  • abstract string constants
  • abstract value, abstract value, abstract value, abstract value, abstract value, abstract value
  • abstract value, of structure
  • abstract values, explicitly given by a trait
  • abstract values, in refinement
  • abstract values, integer types
  • abstract-declarator, defined
  • abstract-declarator, used, abstract-declarator, used, abstract-declarator, used, abstract-declarator, used
  • abstract-string-literal, defined
  • abstract-string-literal, used
  • abstraction, supertype, abstraction, supertype
  • access
  • access declaration
  • access-specifier, defined
  • access-specifier, used, access-specifier, used
  • accesses
  • accesses-clause, defined
  • accesses-clause, used, accesses-clause, used
  • accesses-clause-seq, defined
  • accessibility
  • accessible
  • active
  • address, address
  • ADT
  • allocated
  • allocated, for reference parameters
  • allocated, implicit preconditions
  • allocation, allocation
  • allocation requirements for reference parameters
  • also
  • alternative tokens
  • always-keyword, defined
  • always-keyword, used
  • always-special-symbol, used
  • and
  • and
  • and_eq
  • annotated-iteration-statement, defined
  • annotated-iteration-statement, used
  • annotation
  • annotation, vs. comment
  • annotation-marker, defined
  • annotation-marker, used
  • anonymous ftp
  • any, any
  • argument type
  • array, array, array, array, array, array, array
  • array and pointer, relationship
  • array formal parameter, and pointer
  • array traits
  • array traits, multi-dimensional
  • array variable
  • array, constant
  • array, multi-dimensional
  • array, objects contained in
  • arrays, in modifies clause
  • ASCII
  • asm
  • asm-definition, defined
  • asm-definition, used
  • assert
  • assertion, for loop termination
  • assigned
  • assigned, implicit preconditions
  • assignment operator, implicitly generated
  • assignment-expression, see a C++ grammar
  • assignment-expression, see a C++ grammar for definition
  • assignment-expression, used, assignment-expression, used, assignment-expression, used, assignment-expression, used
  • assume
  • assume-statement, defined
  • assume-statement, used
  • assuming
  • assuming-clause, defined
  • assuming-clause, used
  • assumption
  • assumption, redundant precondition
  • attribute
  • auto
  • b

  • base class
  • base-list, defined
  • base-list, used
  • base-spec, defined
  • base-spec, used
  • base-specifier, defined
  • base-specifier, used
  • be
  • be-list, defined
  • be-list, used
  • behavior
  • behavior program
  • behavior program, example
  • behavior program, vs. higher-order comparisons
  • behavioral interface specification, behavioral interface specification
  • behavioral subtype, behavioral subtype, behavioral subtype
  • behavioral subtype, strong
  • behavioral subtype, strong vs. weak
  • benefits, of Larch/C++
  • bitand
  • bitor
  • blank
  • block
  • BNF
  • bool
  • Bool
  • Boolean trait
  • boolean type
  • brace
  • bracket
  • built in type
  • built-in type
  • built-in-type-name, defined
  • built-in-type-name, used, built-in-type-name, used
  • by, by, by
  • c

  • C++
  • C++ compiler
  • C++ const string, model of
  • C++ function, abstract value of
  • C++ operator symbols
  • C++ reserved words used in Larch/C++, C++ reserved words used in Larch/C++
  • C++ string, model of
  • C++ types, specification of
  • C++-decl-symbol, used
  • C++-operator-symbol, defined
  • C++-operator-symbol, used, C++-operator-symbol, used
  • C++-style-comment, defined
  • C++-style-comment, used
  • C-style-body, defined
  • C-style-body, used
  • C-style-comment, defined
  • C-style-comment, used
  • C-style-end, defined
  • C-style-end, used
  • calls
  • calls-clause, defined
  • calls-clause, used, calls-clause, used
  • calls-clause-seq, defined
  • calls-clause-seq, used
  • carriage return
  • case analysis, case analysis
  • catch
  • char, char, char, char, char
  • char *
  • char * strings
  • char [] strings
  • char, wide
  • char-const-char, defined
  • char-const-char, used
  • char[]
  • character
  • character escape sequence
  • character string, character string
  • character string, abstract
  • character trait
  • character, wide
  • character-constant, defined
  • character-constant, used, character-constant, used
  • characters, characters
  • characters, wide
  • checker
  • checker, for Larch/C++, checker, for Larch/C++
  • checker, for LP, obtaining
  • checker, for LSL
  • checker, for LSL, obtaining
  • choose
  • claim, redundant postcondition
  • claims
  • claims-clause, defined
  • claims-clause, used
  • claims-seq, defined
  • claims-seq, used
  • class, class, class, class, class, class, class
  • class, class, class
  • class constraint
  • class declarations
  • class for exception
  • class invariant
  • class key
  • class member, implicit preconditions for
  • class name, complete, class name, complete
  • class name, qualified, class name, qualified
  • class specification
  • class specification refinement
  • class specification, example
  • class template
  • class template, refinement of
  • class types
  • class types, abstract values
  • class types, automatically defined traits for
  • class types, modifies clause sugar
  • class variable
  • class vs. structure (in Larch/C++)
  • class, abstract
  • class, abstract values of
  • class, automatically constructed trait for
  • class, base
  • class, concrete
  • class, derived, class, derived
  • class, destructor
  • class, member functions and abstract values
  • class, nested refinement
  • class, protection and abstract values
  • class, visibility and abstract values
  • class-head, defined
  • class-head, used
  • class-key, defined
  • class-key, used, class-key, used, class-key, used
  • class-name, defined
  • class-name, used, class-name, used, class-name, used
  • class-specifier
  • class-specifier, defined
  • class-specifier, used
  • client
  • code inheritance
  • coercion function
  • comment
  • comment, defined
  • comment, used
  • comment, vs. annotation
  • compl
  • complete-class-name, defined
  • complete-class-name, used, complete-class-name, used, complete-class-name, used, complete-class-name, used, complete-class-name, used, complete-class-name, used, complete-class-name, used
  • complete-namespace-name, defined
  • complete-namespace-name, used, complete-namespace-name, used
  • complete-template-class-name, defined
  • complete-template-class-name, used, complete-template-class-name, used
  • complete-template-non-class-name, defined
  • complete-template-non-class-name, used
  • complete-type-name, defined
  • complete-type-name, used
  • compound-statement, defined
  • compound-statement, used, compound-statement, used, compound-statement, used
  • concrete class
  • conditional term
  • conjunction
  • const, const, const, const, const
  • const declarations of globals, sorts of (table)
  • const formal parameter declarations and their sorts (table)
  • const string, model of C++
  • constant, constant
  • constant declarations
  • constant object sorts
  • constant pointer
  • constant reference
  • constant string, C++ null terminated
  • constant, character
  • constant, float
  • constant, fractional
  • constant, integer
  • constant, object
  • constant-expression, see a C++ grammar for definition
  • constant-expression, used, constant-expression, used, constant-expression, used
  • constant-initializer, defined
  • constant-initializer, used, constant-initializer, used
  • constants, abstract string
  • constants, floating point
  • constants, integer
  • constants, string
  • ConstObj sort generator
  • ConstObj sorts
  • constrained-set, defined
  • constrained-set, how to use
  • constrained-set, used
  • constraint
  • constraint, for a class
  • constraint-clause, defined
  • constraint-clause, used, constraint-clause, used
  • constraints, inheritance of
  • constructor, constructor, constructor
  • constructor, copy
  • constructor, default, constructor, default
  • constructor, implicit
  • constructs, constructs
  • contained objects, contained objects, contained objects, contained objects
  • contained objects of template container class
  • contained objects, trait
  • contained_objects, contained_objects, contained_objects
  • container class, contained objects of
  • container membership assumption trait
  • container objects trait
  • containment
  • context-dependent-keyword, defined
  • context-dependent-keyword, used
  • conversion-function-id, defined
  • conversion-function-id, used
  • copy constructor
  • copy constructor, implicitly generated
  • correctly implements
  • correctness, partial
  • correctness, total
  • ctor-declarator, defined
  • ctor-declarator, used, ctor-declarator, used, ctor-declarator, used
  • ctor-initializer, defined
  • ctor-initializer, used
  • curly bracket
  • cv-qualifier, defined
  • cv-qualifier, used, cv-qualifier, used
  • cv-qualifier-seq, defined, cv-qualifier-seq, defined
  • cv-qualifier-seq, used
  • d

  • data member
  • data member, exposed
  • data member, implicit preconditions for
  • data member, public
  • data member, specifying in a class
  • data members
  • data members, inheritance of
  • datatype
  • deallocation, deallocation, deallocation
  • deallocation, and modifies-clause
  • decimal-constant, defined
  • decimal-constant, used, decimal-constant, used
  • decl-qualifier, defined
  • decl-qualifier, used
  • decl-qualifier-seq, defined
  • decl-qualifier-seq, used
  • decl-specifier, defined
  • decl-specifier, used
  • decl-specifier-seq, defined
  • decl-specifier-seq, used, decl-specifier-seq, used, decl-specifier-seq, used, decl-specifier-seq, used, decl-specifier-seq, used, decl-specifier-seq, used
  • declaration, declaration, declaration
  • declaration of exceptions
  • declaration specifier
  • declaration, access
  • declaration, array
  • declaration, class
  • declaration, constant
  • declaration, defined
  • declaration, for specification purposes only
  • declaration, function
  • declaration, reference
  • declaration, refinement of
  • declaration, samples
  • declaration, structure (struct)
  • declaration, union
  • declaration, used, declaration, used, declaration, used, declaration, used, declaration, used, declaration, used
  • declaration-seq, defined
  • declaration-seq, used, declaration-seq, used, declaration-seq, used
  • declarations and sorts for global variables, summary (table)
  • declarations, of globals with const (table)
  • declarations, of globals, and their sorts (table)
  • declarator, defined
  • declarator, used, declarator, used, declarator, used, declarator, used
  • declarator-qualifier, defined
  • declarator-qualifier, used
  • decreasing
  • decreasing-seq, defined
  • decreasing-seq, used
  • default constructor, default constructor
  • definition, definition
  • definition, function
  • delete
  • delete []
  • delete operator vs. destructor
  • deletion of objects
  • dependency, example
  • dependent object
  • depends
  • depends-clause, defined
  • depends-clause, example use of, depends-clause, example use of
  • depends-clause, used, depends-clause, used
  • deprecated
  • dereferencing a pointer
  • derived class, derived class
  • derived class, how to specify
  • described, by a modifies-clause
  • described, for a trashes clause
  • description, informal
  • design decision, recording, design decision, recording, design decision, recording, design decision, recording, design decision, recording, design decision, recording
  • destructor
  • destructor, implicitly generated
  • destructor, specification of
  • detailed design decision, recording, detailed design decision, recording, detailed design decision, recording, detailed design decision, recording, detailed design decision, recording, detailed design decision, recording
  • detailed design, recording
  • determinism, in a function specification
  • digit, defined
  • digit, used, digit, used
  • direct-abstract-declarator, defined
  • direct-abstract-declarator, used
  • direct-declarator, defined
  • direct-declarator, used
  • distinguishing between returning and exceptions
  • do
  • domain, of a function or relation
  • DOS, port of Larch/C++ for
  • double, double, double, double
  • double, double
  • dtor-name, defined
  • dtor-name, used
  • dynamic binding
  • e

  • e
  • E
  • Eiffel
  • elaborated-type-specifier, defined
  • elaborated-type-specifier, used
  • Ellis, M.A.
  • else
  • ensures
  • ensures-clause, defined
  • ensures-clause, used, ensures-clause, used
  • ensures-clause-seq, defined
  • ensures-clause-seq, used
  • enum, enum, enum
  • enum-name, defined
  • enum-name, used
  • enum-specifier, defined
  • enumeration, enumeration
  • enumerator
  • enumerator-definition, defined
  • enumerator-definition, used
  • enumerator-definition-list, defined
  • enumerator-definition-list, used
  • environment
  • eq-opr, defined
  • eq-opr, used
  • equality-term, defined
  • equality-term, used
  • escape-sequence, defined
  • escape-sequence, used
  • eval trait function
  • everything, everything, everything, everything, everything, everything
  • example
  • example, in function specification
  • example, used
  • example-seq, defined
  • example-seq, used
  • examples, guidelines for
  • exception, class for
  • exception-decl, defined
  • exception-decl, used
  • exception-declaration, defined
  • exception-declaration, used
  • exceptions, declaration of
  • exceptions, specification of
  • expected-trait-list, defined
  • expected-trait-list, used
  • expects
  • expects-clause, defined
  • expects-clause, used, expects-clause, used
  • explicit, explicit
  • explicit-instantiation, defined
  • explicit-instantiation, used
  • explicit-specialization, defined
  • explicit-specialization, used
  • explicitly given trait
  • explicitly-given traits, and weak behavioral subtyping
  • exponent-indicator, defined
  • exponent-indicator, used
  • exponent-part, defined
  • exponent-part, used
  • exposed data member
  • expression, additional keywords for
  • expression, constant
  • expression, defined and see a C++ grammar
  • expression, see a C++ grammar for definition
  • expression, used, expression, used
  • expression-list, defined, expression-list, defined
  • expression-list, used, expression-list, used, expression-list, used
  • extern, extern, extern, extern
  • external linkage
  • f

  • F
  • f
  • false
  • fcnId, defined
  • fcnId, used, fcnId, used
  • field name
  • field, of a class value
  • field, of a structure value
  • field, of a union
  • file
  • file suffix for Larch/C++
  • float, float, float
  • float, float
  • float-suffix, defined
  • float-suffix, used
  • floating point constants
  • floating-constant, defined
  • floating-constant, used
  • FloatingPoint trait
  • for, for, for
  • for all
  • for some
  • formal documentation
  • formal parameter
  • formal parameter declarations and their sorts (table)
  • formal parameter, complex, sorts of (table)
  • formal parameters, const, sorts of (table)
  • formal parameters, sorts of (table)
  • formal specification, reasons for using
  • formality, tuning
  • formfeed
  • fractional-constant, defined
  • fractional-constant, used
  • frame axiom, frame axiom, frame axiom
  • frame axioms
  • frame, defined
  • frame, used
  • Fresco
  • fresh, fresh
  • friend, friend, friend
  • friend
  • friendship in classes
  • ftp
  • fun-body, defined
  • fun-body, used
  • fun-interface, defined
  • fun-interface, used, fun-interface, used, fun-interface, used
  • fun-interface-list, defined
  • fun-interface-list, used, fun-interface-list, used
  • fun-spec-body, defined
  • fun-spec-body, used, fun-spec-body, used, fun-spec-body, used, fun-spec-body, used
  • fun-spec-boyd, used
  • fun-try-block, used
  • function, function
  • function declaration
  • function definition
  • function interface
  • function specification scope
  • function template
  • function template, refinement of
  • function type, abstract model of
  • function, higher-order
  • function, interface with const
  • function, member
  • function, parameter specification
  • function, pointer
  • function, specification of
  • function-definition, defined
  • function-definition, used, function-definition, used
  • function-name, defined
  • function-name, used
  • function-names, defined
  • function-names, used
  • function-specifier, defined
  • function-specifier, used
  • function-try-block, defined
  • g

  • g++, attribute definitions
  • gcc, attribute definitions
  • getting, the LP checker
  • getting, the LSL checker
  • ghost variable
  • ghost variable, in class specification
  • global array variable
  • global class variable
  • global pointer variable
  • global reference variable
  • global structure (struct) variable
  • global union variable
  • global variable, global variable
  • global variables, sorts of (table)
  • global variables, sorts of, summary (table)
  • global variables, with const, sorts (table)
  • GNU
  • goals, goals
  • grammar, conventions for lists
  • guarded-statement, defined
  • guarded-statement, used
  • h

  • Handbook, for LSL
  • handbook, for LSL
  • handler, defined
  • handler, used
  • handler-seq, defined
  • handler-seq, used
  • hex-constant, defined
  • hex-constant, used
  • hex-digit, defined
  • hex-digit, used, hex-digit, used
  • hex-indicator, defined
  • hex-indicator, used
  • hiding
  • higher-order functions
  • higher-order-comparison, defined
  • history constraint, example
  • history constraint, inheritance for strong behavioral subtypes
  • history constraints, inheritance of
  • Hoare, Hoare
  • home page, for Larch
  • homomorphism property
  • i

  • id-expression, defined
  • id-expression, used, id-expression, used
  • ident()
  • identifier, defined
  • identifier, possible meanings
  • identifier, sort
  • identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used, identifier, used
  • if then else
  • illustrating, function specifications
  • immutable
  • implementation
  • implementations and invariants
  • implements
  • implicit preconditions
  • implicitly generated assignment operator
  • implicitly generated constructor
  • implicitly generated copy constructor
  • implicitly generated destructor
  • implicitly generated member functions
  • implicitly generated members, suppressing
  • implies
  • include files
  • including, a trait
  • incomplete specification, defined
  • incomplete specification, examples for
  • incomplete, function specification
  • incompleteness, in a function specification
  • infix operator, infix operator
  • influences, on Larch/C++ evolution
  • informal specification, example
  • informal, modifies clause
  • informal-comment, defined
  • informal-comment, used
  • informal-comment-body, defined
  • informal-comment-body, used
  • informal-desc, defined
  • informal-desc, no longer used for traits
  • informal-desc, used
  • informally, informally, informally
  • inheritance
  • inheritance of data members
  • inheritance of history constraints
  • inheritance of history constraints, for weak behavioral subtypes
  • inheritance of invariants
  • inheritance of specifications
  • inheritance of specifications, desugaring
  • inheritance of specifications, related work
  • inheritance of specifications, strengthening
  • inheritance, not for a uses-clause
  • inheritance, of specifications
  • inheritance, of specifications, details
  • inheritance, specifying code
  • init-declarator, defined
  • init-declarator, used, init-declarator, used, init-declarator, used
  • init-declarator-list, defined
  • init-declarator-list, used
  • initial value
  • initializer, defined
  • initializer, used, initializer, used
  • initializer-clause, defined
  • initializer-clause, used
  • initializer-list, defined
  • initializer-list, used
  • inline
  • instance
  • instance value
  • instance variables
  • int, int, int, int
  • integer constants
  • Integer trait
  • integer traits, summary
  • integer types
  • integer-constant, defined
  • integer-constant, used
  • integer-suffix, defined
  • integer-suffix, used
  • integers, unsigned
  • interface, interface, interface
  • interface for exceptions
  • interface of a function with const
  • interface specification
  • interface specification module
  • interface specifications of built-in types
  • interface, access to members of
  • interface, defined
  • interface, private
  • interface, protected
  • interface, public
  • internal linkage
  • international character set support
  • invariant
  • invariant, for a class
  • invariant-clause, defined
  • invariant-clause, used, invariant-clause, used
  • invariants, inheritance of
  • is
  • iteration statement, annotated
  • iteration-statement, used
  • k

  • keyword
  • keyword, defined
  • keyword, used
  • keyword, using one as an identifier
  • keywords
  • Keywords in Predicates
  • keywords, added to C++, keywords, added to C++
  • keywords, recognized everywhere
  • l

  • l, l
  • L, L, L, L
  • Larch
  • Larch Prover, obtaining
  • Larch Shared Language (LSL)
  • Larch Shared Language Checker
  • Larch style specification language
  • Larch, global home page for
  • larch-cpp-clause, defined
  • larch-cpp-clause, used
  • Larch-style specification
  • Larch/C
  • Larch/C++ reserved words not in C++, Larch/C++ reserved words not in C++
  • Larch/C++ reserved words recognized everywhere
  • Larch/C++ status and plans
  • Larch/C++, evolution
  • Larch/C++, ftp
  • Larch/C++, goals
  • Larch/C++, obtaining
  • Larch/C++, plans
  • Larch/C++, status
  • LARCH_PATH environment variable
  • LCL
  • lcpp, specification checker
  • lcpp-primary, defined
  • lcpp-primary, used
  • Leino, Leino
  • let
  • let scope
  • let-clause, defined
  • let-clause, used
  • letter, defined
  • letter, used, letter, used
  • letter-or-digit, defined
  • letter-or-digit, used, letter-or-digit, used
  • lexeme, defined
  • lexeme, used
  • lexical conventions
  • liberal specification
  • liberally, liberally, liberally
  • linkage
  • linkage, external
  • linkage, internal
  • linkage-declaration, defined
  • linkage-declaration, used
  • list vs. sequence, in grammar
  • literal
  • literal, defined
  • literal, used, literal, used
  • LM3, LM3
  • local scope
  • location
  • logical-opr, defined
  • logical-opr, used
  • logical-term, defined
  • logical-term, used, logical-term, used
  • long, long, long, long, long
  • long double, long double
  • long double
  • long integer trait
  • long integers
  • long-suffix, defined
  • long-suffix, used
  • loop invariant
  • loop statement, annotated
  • looping, specification of
  • LP, obtaining
  • LP, the Larch Prover
  • LSL, LSL
  • LSL checker, LSL checker
  • LSL checker, obtaining
  • LSL checker, use
  • LSL Handbook
  • LSL initialization for Larch/C++
  • LSL operators, reserved
  • LSL trait
  • LSL tuple, LSL tuple
  • lsl, LSL trait checker
  • lsl-constant, defined
  • lsl-formal, defined
  • lsl-formal, used
  • lsl-instance-actuals, defined
  • lsl-instance-actuals, used
  • lsl-op, defined
  • lsl-op, reserved
  • lsl-op, used, lsl-op, used
  • lsl-op-term, defined
  • lsl-op-term, used, lsl-op-term, used
  • lsl-signature, defined
  • lsl-signature, used
  • lsl-sort, defined
  • lsl-sort, used
  • lsl-sort-list, defined
  • lsl-sort-list, used
  • lvalue
  • m

  • macro, for ident
  • maintaining
  • maintaining-seq, defined
  • maintaining-seq, used
  • mem-initializer, defined
  • mem-initializer, used
  • mem-initializer-id, defined
  • mem-initializer-id, used
  • member function
  • member functions, implicit
  • member, implicit preconditions for
  • member, of a structure
  • member, pointer to, member, pointer to
  • member-declaration, defined
  • member-declaration, used, member-declaration, used
  • member-declarator, defined
  • member-declarator, used
  • member-declarator-list, defined
  • member-declarator-list, used
  • member-seq, defined
  • member-seq, used, member-seq, used, member-seq, used
  • message send
  • microsyntax, defined
  • model, of a struct, user-defined
  • model, of objects
  • model, of states
  • model-oriented specification
  • modifies
  • modifies, modifies, modifies, modifies, modifies
  • modifies clause, and arrays
  • modifies clause, and pointers
  • modifies clause, informal
  • modifies, in constructor
  • modifies, omitted
  • modifies-clause
  • modifies-clause, defined
  • modifies-clause, in constructor
  • modifies-clause, in destructor
  • modifies-clause, used, modifies-clause, used
  • modifies-clause-seq, defined
  • modifies-clause-seq, used
  • modular reasoning
  • modular specification
  • modular verification
  • module, module
  • modules, namespace
  • MS-DOS, port of Larch/C++ for
  • multi-dimensional array trait
  • multicharacter constant
  • mutable
  • mutable object
  • mutates
  • mutation, mutation
  • n

  • name spaces, for identifiers
  • name, identity between class and sort name
  • namespace
  • namespace
  • namespace name, complete
  • namespace name, qualified
  • namespace, refinement of
  • namespace-alias-definition, defined
  • namespace-alias-definition, used, namespace-alias-definition, used
  • namespace-alias-name, defined
  • namespace-alias-name, used, namespace-alias-name, used, namespace-alias-name, used
  • namespace-definition, defined
  • namespace-definition, used
  • namespace-name, defined
  • namespace-name, used
  • narrowing
  • natural numbers
  • nested class, refinement of
  • nested-name-specifier, defined
  • nested-name-specifier, used, nested-name-specifier, used, nested-name-specifier, used
  • new
  • new []
  • newline, newline
  • newline, defined
  • newline, used, newline, used, newline, used
  • nominal type
  • non-at-newline, defined
  • non-at-newline, used
  • non-at-star, defined
  • non-at-star, used
  • non-class-type-name, used
  • non-escape-code, defined
  • non-escape-code, used
  • non-newline, defined
  • non-newline, used, non-newline, used
  • non-nl-white-space, defined
  • non-nl-white-space, used, non-nl-white-space, used
  • non-nl-whitespace, used
  • non-percent, defined
  • non-percent, used
  • non-percent-right-paren, defined
  • non-percent-right-paren, used
  • non-right-paren, defined
  • non-right-paren, used
  • non-semi-newline, defined
  • non-semi-newline, used
  • non-slash, defined
  • non-slash, used
  • non-star, defined
  • non-star, used
  • non-star-slash, defined
  • non-star-slash, used
  • non-std-esc, defined
  • non-std-esc, used
  • non-type-parameter-decl, defined
  • non-type-parameter-decl, used
  • nondeterminism, in a function specification
  • nondeterministic-choice, defined
  • nondeterministic-choice, used
  • nondeterministic-if, defined
  • nondeterministic-if, used
  • nontermination
  • normal-char, defined
  • normal-char, used, normal-char, used
  • not
  • not_eq
  • nothing, nothing, nothing
  • null terminated const string
  • null terminated string
  • nullTerminated trait function
  • o

  • Obj sorts
  • object, object, object, object, object, object, object
  • object deallocation
  • object identifier
  • object trashing
  • object, constant
  • object, contained
  • object, destruction
  • object, mutable
  • object, reachable
  • object, untyped model of
  • objects, abstract values of
  • objects, constant
  • objects, contained
  • objects, sorts of
  • obtaining, the LP checker
  • obtaining, the LSL checker
  • octal-code, defined
  • octal-code, used
  • octal-constant, defined
  • octal-constant, used
  • octal-digit, defined
  • octal-digit, used, octal-digit, used
  • on, on
  • one-to-nine, defined
  • one-to-nine, used
  • op-char, defined
  • op-char, used
  • operation
  • operator
  • operator
  • operator character
  • operator symbols, C++
  • operator, infix
  • operator, of LSL
  • operator, postfix
  • operator, prefix
  • operator-function-id, defined
  • operator-function-id, used
  • or, or
  • or
  • or_eq
  • original-class-name, defined
  • original-class-name, used, original-class-name, used, original-class-name, used, original-class-name, used
  • original-enum-name, defined
  • original-enum-name, used, original-enum-name, used
  • original-namespace-name, defined
  • original-namespace-name, used, original-namespace-name, used, original-namespace-name, used, original-namespace-name, used
  • OS/2, port of Larch/C++ for
  • overloading, dynamic
  • overloading, of trait functions
  • overview
  • p

  • param-qualifier, defined
  • param-qualifier, used, param-qualifier, used
  • parameter, formal
  • parameter, sort
  • parameter, to a template
  • parameter, value, parameter, value
  • parameter-declaration, defined
  • parameter-declaration, used
  • parameter-declaration-clause, defined
  • parameter-declaration-clause, used
  • parameter-declaration-list, defined
  • parameter-declaration-list, used
  • parameter-initializer, defined
  • parameter-initializer, used
  • parameters, formal, sorts of (table)
  • parser, for Larch/C++
  • partial correctness, partial correctness
  • percents-non-right-paren, defined
  • percents-non-right-paren, used
  • perspectives, recording
  • plans, for Larch/C++
  • pointer, pointer, pointer, pointer, pointer
  • pointer and array, relationship
  • pointer dereference
  • pointer to a constant
  • pointer to member, pointer to member
  • pointer variable
  • pointer, and array
  • pointer, and array formal
  • pointer, constant
  • pointer, deallocation via
  • pointer, differences from LCL
  • pointer, to array
  • pointer, to function
  • pointer, valid
  • pointers, in modifies clause
  • polymorphic
  • polymorphism, subtype
  • post
  • post, post
  • post-cond, defined
  • post-cond, used
  • post-state, post-state
  • post-state, for a history constraint
  • post-value
  • postcondition, postcondition, postcondition
  • postcondition, redundant
  • postfix operator, postfix operator
  • postfix-expression, defined and see a C++ grammar
  • postfix-expression, used
  • pragma
  • pragma
  • pragma, defined
  • pragma, used
  • pre
  • pre, pre
  • pre pointer trait
  • pre-cond, defined
  • pre-cond, used
  • pre-state, pre-state
  • pre-state, for a history constraint
  • pre-value
  • precondition, precondition, precondition
  • precondition, redundant
  • preconditions, implicit
  • predicate, defined
  • predicate, used, predicate, used, predicate, used, predicate, used, predicate, used
  • predicate-keyword, used
  • predicate-symbol, defined
  • predicate-symbol, used
  • prefix operator, prefix operator
  • preprocessing
  • primary, defined
  • primary, used
  • primary-suffix, defined
  • primary-suffix, used
  • primitive, defined
  • primitive, used
  • private, private, private
  • private
  • private interface
  • private members, granting friendship to
  • procedure, abstract model of
  • procedure, higher-order
  • program
  • program, abstract
  • program, behavior
  • proof of correctness, for loops
  • protected, protected, protected
  • protected interface
  • ptr-operator, defined
  • ptr-operator, used
  • public, public
  • public data member
  • public interface
  • punctuation symbols
  • punctuation symbols, used in C++ declarations
  • pure specifier
  • pure virtual function
  • pure virtual, member function
  • pure virtual, removed
  • q

  • qualified-id, defined
  • qualified-id, used, qualified-id, used
  • quantified varId, sort
  • quantified-list, defined
  • quantified-list, used
  • quantifier scope, quantifier scope
  • quantifier, defined
  • quantifier, used
  • quantifier-sym, defined
  • quantifier-sym, used
  • quantifiers, eliminating
  • r

  • reach, reach, reach
  • reachability
  • reasoning, modular
  • reasons, for formal documentation
  • record
  • recording detailed design
  • recording detailed design decision, recording detailed design decision, recording detailed design decision, recording detailed design decision, recording detailed design decision
  • recording detailed design decision, recording
  • redundancy, in function specifications
  • redundancy, in history constraints
  • redundancy, in postcondition
  • redundancy, in precondition
  • redundantly, redundantly, redundantly, redundantly, redundantly, redundantly, redundantly, redundantly, redundantly, redundantly
  • reference, reference
  • reference parameters, implicit requirement
  • reference to a constant
  • reference variable
  • reference, constant
  • refinable-id, defined
  • refinable-id, used
  • refine
  • refine-prefix, defined
  • refine-prefix, used, refine-prefix, used
  • refinement
  • refinement calculus
  • refinement, of class specifications
  • refinement, of namespace
  • refinement, of nested class
  • refinement, of template
  • refinement, vs. subtyping
  • refinement-declaration, defined
  • refinement-declaration, used
  • refinement-member-decl, defined
  • refinement-member-decl, used
  • register, register
  • related work, on inheritance of specifications
  • release, obtaining the Larch/C++
  • release, of Larch/C++
  • renaming, defined
  • renaming, used
  • replace, defined
  • replace, used
  • replace-list, defined
  • replace-list, used, replace-list, used
  • representation
  • represents
  • represents-clause, defined
  • represents-clause, example use of, represents-clause, example use of
  • represents-clause, used, represents-clause, used
  • req-frame-ens, defined, req-frame-ens, defined
  • req-frame-ens, used
  • requirement, on template argument
  • requires
  • requires-clause, defined
  • requires-clause, used, requires-clause, used
  • requires-clause-seq, defined
  • requires-clause-seq, used
  • reserved words
  • reserved words, for C++ statements and expressions
  • reserved words, recognized everywhere
  • reserved words, used in a term or predicate
  • RESOLVE
  • result, result, result, result, result
  • result
  • result, sort of (table)
  • returning, instead of signaling
  • returns, returns
  • rvalue
  • s

  • satisfaction
  • satisfies
  • satisfies
  • satisfies, for function specifications, satisfies, for function specifications
  • sc-bracketed, defined
  • sc-bracketed, used
  • scope
  • scope rules
  • scope unit
  • scope, function specification
  • scope, let
  • scope, local
  • scope, of a let-clause
  • scope, quantifier, scope, quantifier
  • secondary, defined
  • secondary, used
  • selection, defined
  • selection, used
  • self, self, self, self, self
  • self, data members
  • self, in class specifications
  • send, of message
  • sequence vs. list, in grammar
  • short, short, short, short
  • short integer trait
  • short integers
  • sign, defined
  • sign, used
  • signaling an exception
  • signature, signature
  • signature, example
  • signed, signed, signed, signed, signed
  • signed integer trait, signed integer trait
  • simple-id, defined
  • simple-id, used, simple-id, used, simple-id, used
  • simple-type-name, defined
  • simple-type-name, used
  • simulates
  • simulates-clause, defined
  • simulates-clause, example of
  • simulates-clause, used
  • simulation function
  • simulation function, homomorphism property
  • simulation function, use in inheritance
  • simulation functions, and state
  • sizeof
  • sort, sort, sort, sort, sort
  • sort checking
  • sort of result (table)
  • sort, for a class
  • sort, of C++ strings
  • sort-instance-actuals, defined
  • sort-instance-actuals, used
  • sort-name, defined
  • sort-name, used, sort-name, used, sort-name, used, sort-name, used, sort-name, used
  • sort-or-type, defined
  • sort-or-type, used
  • sorts and types, association of, example, sorts and types, association of, example
  • sorts for complex declarations of formal parameters
  • sorts for complex declarations of global variables (table)
  • sorts of global variables (table)
  • sorts of objects
  • sorts, of constant objects
  • sorts, of global variables using const (table)
  • space, name
  • spec, spec
  • spec-case
  • spec-case, defined, spec-case, defined
  • spec-case, removed form
  • spec-case, used
  • spec-case-seq
  • spec-case-seq, defined
  • spec-case-seq, used
  • spec-decl, defined
  • spec-decl, example in class specifications
  • spec-decl, used, spec-decl, used, spec-decl, used
  • SPEC_PATH, see LARCH_PATH
  • special-function-declarator, defined
  • special-function-declarator, used, special-function-declarator, used
  • special-symbol, defined, special-symbol, defined, special-symbol, defined
  • special-symbol, used
  • specification declaration
  • specification declaration, for a class, example, specification declaration, for a class, example
  • specification inheritance, specification inheritance
  • specification inheritance, details
  • specification module
  • specification of exceptions
  • specification styles
  • specification variable
  • specification variable, in class specification
  • specification variables, and inheritance
  • specification, examples in
  • specification, liberal
  • specification, modular
  • specification, of a class
  • specification, of a function
  • specification, of an interface's behavior
  • specification, of interface behavior
  • specification, partial
  • specification, refinement of
  • specification-statement, defined
  • specification-statement, used
  • square bracket
  • star-or-op-char, defined
  • star-or-op-char, used
  • stars-non-slash, defined
  • stars-non-slash, used
  • state, state, state, state, state
  • state, and simulation functions
  • state, model of
  • State, sort
  • state, trait for
  • state, values from objects in
  • state-function
  • state-function, defined
  • state-function, used
  • statement, additional keywords for
  • statement, defined
  • statement, used
  • statement-seq, used
  • states, in trait functions
  • states, names for
  • static, static
  • static type
  • status, of Larch/C++
  • std-esc, defined
  • std-esc, used, std-esc, used
  • stmt-exp-only-keyword, defined
  • stmt-exp-only-keyword, used
  • storage-class-specifier, defined
  • storage-class-specifier, used
  • store-ref, defined
  • store-ref, used, store-ref, used, store-ref, used, store-ref, used
  • store-ref-list, defined
  • store-ref-list, used, store-ref-list, used, store-ref-list, used, store-ref-list, used, store-ref-list, used
  • strengthening specifications in derived classes
  • string
  • string (of characters)
  • string (of characters), abstract
  • string constants
  • string, abstract
  • string, C++ null terminated
  • string, in C++
  • string, model of C++
  • string, unsigned character
  • string, wide
  • string, wide character
  • string-character, defined
  • string-character, used, string-character, used
  • string-literal, defined
  • string-literal, used, string-literal, used, string-literal, used, string-literal, used
  • strong behavioral subtype
  • strong behavioral subtype, and inheritance of history constraints
  • Stroustrup, B.
  • struct
  • struct, struct, struct, struct, struct, struct, struct
  • struct, differences from LCL
  • struct, specifying your own model of
  • structure declarations
  • structure types
  • structure types, abstract values
  • structure types, automatically defined traits for
  • structure types, differences from LCL
  • structure types, modifies clause sugar
  • structure variable
  • structure, abstract value of
  • structure, automatically constructed trait for
  • structure, field
  • structure, member functions and abstract values
  • structure, protection and abstract values
  • structure, specification of
  • structure, state functions applied to
  • structure, visibility and abstract values
  • structure. vs class (in Larch/C++)
  • style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline, style guideline
  • styles, of specification
  • subclass, subclass
  • subclass, how to specify
  • subtype, subtype
  • subtype, behavioral, subtype, behavioral
  • subtype, how to specify
  • subtype, strong behavioral,
  • subtyping
  • suffix, for Larch/C++
  • sugar, syntactic for fresh
  • sugar, syntactic in modifies-clause
  • sugars, preconditions in functions
  • summary of integer traits
  • summary of sorts for formal parameters (table)
  • supertype, supertype
  • supertype abstraction, supertype abstraction
  • supertype abstraction, in specification
  • supertype, defined
  • supertype, used
  • supertype-list, defined
  • supertype-list, used
  • suppressing implicitly generated members
  • symbols, for C++ operators
  • symbols, punctuation in C++ declarations
  • symbols, reserved, from C++
  • symbols, special
  • syntactic sugar in modifies-clause
  • syntactic sugar for fresh
  • syntax notations
  • t

  • tab
  • template, template, template
  • template argument, requirements on
  • template class trait, example
  • template class, example, template class, example
  • template container class, contained objects
  • template function, example
  • template, refinement of
  • template-argument, defined
  • template-argument, used
  • template-argument-list, defined
  • template-argument-list, used
  • template-class-instance, defined
  • template-class-instance, used, template-class-instance, used, template-class-instance, used, template-class-instance, used
  • template-class-name, defined
  • template-class-name, used, template-class-name, used, template-class-name, used, template-class-name, used
  • template-declaration, defined
  • template-declaration, used
  • template-init, defined
  • template-init, used
  • template-instance, defined
  • template-instance, used
  • template-instance-actuals, defined
  • template-instance-actuals, used
  • template-non-class-instance, defined
  • template-non-class-instance, used
  • template-non-class-name, defined
  • template-non-class-name, used, template-non-class-name, used, template-non-class-name, used
  • template-parameter, defined
  • template-parameter, used
  • template-parameter-list, defined
  • template-parameter-list, used
  • template-using-list, defined
  • templates, simple example
  • term, additional keywords for
  • term, defined
  • term, used, term, used, term, used, term, used, term, used, term, used, term, used, term, used
  • term-list, defined
  • term-list, used, term-list, used, term-list, used
  • term-only-keyword, defined
  • term-only-keyword, used
  • terminates, terminates
  • termination, termination, termination
  • termination function for loop
  • then
  • there exists
  • this, this
  • threatened variable
  • throw
  • throw declarations
  • throwing an exception
  • thrown, thrown
  • throws, throws
  • to_int
  • to_int trait function
  • to_LSL_Bool trait function
  • token
  • token, defined
  • token, used
  • tools
  • tools, for Larch/C++
  • tools, using
  • top-level, defined
  • top-level, used
  • total correctness, total correctness
  • trait, trait
  • trait for double
  • trait for float
  • trait for long double
  • trait for void
  • trait for wchar_t
  • trait function
  • trait functions, use instead of quantifiers
  • trait, defined
  • trait, for a class
  • trait, for a class template
  • trait, for pointers
  • trait, for pointers to arrays
  • trait, for pointers to member arrays
  • trait, for pointers to members
  • trait, for pointers to objects
  • trait, for struct
  • trait, for typed objects
  • trait, how it determines abstract values
  • trait, used, trait, used
  • trait-list, defined
  • trait-list, used, trait-list, used
  • trait-name, defined
  • trait-name, used
  • trait-or-deref-list, defined
  • trait-or-deref-list, used
  • traits for built-in types
  • traits for floating point types
  • traits for integer types
  • traits, finding
  • traits, for classes
  • traits, for integer types
  • traits, using them
  • trashed, trashed, trashed
  • trashed, concept of
  • trashes
  • trashes-clause, defined
  • trashes-clause, used, trashes-clause, used
  • trashes-clause-seq, defined
  • trashes-clause-seq, used
  • trashing, and modifies-clause
  • trashing, how to specify
  • trick, for specifying derived classes
  • true
  • try
  • tuning of formality
  • tuple, LSL, tuple, LSL
  • type
  • type definition
  • type equivalence
  • type name, simple
  • type specifier, elaborated
  • type to sort mapping, type to sort mapping, type to sort mapping, type to sort mapping, type to sort mapping
  • type, abstract
  • type, built in
  • type, built-in
  • type, nominal
  • type, static
  • type-arg-name, defined
  • type-arg-name, used
  • type-id, defined
  • type-id, used, type-id, used, type-id, used, type-id, used, type-id, used
  • type-init, defined
  • type-init, used
  • type-list, defined
  • type-list, used
  • type-name, defined
  • type-name, used
  • type-parameter, defined
  • type-parameter, used
  • type-specifier, defined
  • type-specifier, used, type-specifier, used
  • type-specifier-seq, defined
  • type-specifier-seq, used, type-specifier-seq, used, type-specifier-seq, used, type-specifier-seq, used
  • typedef, typedef
  • typedef-class-name, defined
  • typedef-class-name, used, typedef-class-name, used
  • typedef-enum-name, defined
  • typedef-enum-name, used, typedef-enum-name, used, typedef-enum-name, used
  • typedef-non-class-or-enum-name, defined
  • typedef-non-class-or-enum-name, used, typedef-non-class-or-enum-name, used, typedef-non-class-or-enum-name, used
  • typename, typename, typename
  • u

  • u
  • U
  • unassigned
  • unassigned, how to specify making an object
  • unchanged, unchanged
  • union, union, union, union, union, union
  • union declarations
  • union variable
  • union, abstract value of
  • union, differences from LCL
  • union, example trait for
  • union, specification of
  • Unix, port of Larch/C++ for
  • unqualified-id, defined
  • unqualified-id, used, unqualified-id, used, unqualified-id, used, unqualified-id, used
  • unsigned
  • unsigned, unsigned, unsigned, unsigned
  • unsigned char
  • unsigned int
  • unsigned long
  • unsigned short
  • unsigned-suffix, defined
  • unsigned-suffix, used
  • unsignedChar sort
  • unsignedInt sort
  • unsignedInt trait function
  • unsignedLong sort
  • unsignedLong trait function
  • unsignedShort sort
  • unsignedShort trait function
  • untyped objects
  • usefulness, of Larch/C++
  • user-defined model of a struct
  • uses
  • uses, of Larch/C++
  • uses-clause, and class templates
  • uses-clause, defined
  • uses-clause, in refinement
  • uses-clause, used, uses-clause, used, uses-clause, used, uses-clause, used
  • uses-seq, defined
  • uses-seq, used
  • using, using
  • using
  • using-declaration, defined
  • using-declaration, used, using-declaration, used, using-declaration, used
  • using-directive, defined
  • using-directive, used, using-directive, used
  • using-trait-list, defined
  • using-trait-list, used, using-trait-list, used
  • utility, of Larch/C++
  • v

  • valid pointer
  • value, value, value
  • value parameter, value parameter
  • value, abstract, value, abstract
  • value, initial
  • variable
  • variable, array
  • variable, class
  • variable, global
  • variable, global, declaration of
  • variable, pointer
  • variable, reference
  • variable, structure (struct)
  • variable, union
  • variables, global, sorts of (table)
  • variant record types
  • varId, defined
  • varId, used, varId, used
  • VDM
  • verification
  • verification, modular
  • vertical tab
  • viewpoint
  • virtual, virtual, virtual
  • virtual function, pure
  • virtual, pure
  • visibility
  • visible state, visible state
  • vocabulary
  • void, void, void
  • void type
  • volatile
  • w

  • wchar_t, wchar_t
  • weak behavioral subtype, example
  • weak behavioral subtypes and inheritance of history constraints
  • weak behavioral subtyping
  • weakly
  • well-defined
  • where
  • where clause
  • where-body, defined
  • where-body, used
  • where-clause, defined
  • where-clause, used
  • where-seq, defined
  • where-seq, used
  • while
  • white space, white space
  • white-space, defined
  • white-space, used
  • wide character type interface specification
  • wide characters
  • wide-character string
  • widening
  • Wills
  • Windows 95, port of Larch/C++ for
  • Windows 97, port of Larch/C++ for
  • Windows NT, port of Larch/C++ for
  • with
  • word, reserved
  • worlds, that identifiers live in
  • WWW page, for Larch
  • x

  • x, x
  • X
  • xor
  • xor_eq
  • z

  • Z
  • {

  • {, {, {, {, {, {, {, {
  • {}
  • |

  • |, |
  • |=
  • ||, ||
  • }

  • }, }, }, }, }, }, }, }
  • ~

  • ~, ~
  • ~=, ~=

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