Go to the first, previous, next, last section, table of contents.
!
!, !, !
!=, !=, !=
"
", ", "
#
#, #
#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.