abort, 343 (debugger), 995 (debugger), 1160 (debugger)
abstraction, see model checking
allow-dir, 602, 615, 1039
allow-files, 600, 608, 610, 1040
allow-processes, 601, 629, 632, 1041
always-advise, 1042
ansi-color, 1043
AProVe, 728
array, 590–591
ASF+SDF, 153n, 245n, 966
assoc, 140, 170, 178, 183, 476, 1009, 1016, 1018, 1028, 1032, 1067
assoc-unif-depth, 1045
associative, see assoc
attribute, 168–239
equational, 169–191
statement, 240–249
batch, 1046
Boolean value, 519–526
break point, 989, 1006
break select, 990, 1159
bubble, 965
CafeOBJ, 21
cd, 1176
ceq, 150
ChC, 15, 730
check, 871, 1094
Church-Rosser, 263
context-sensitive, 271
ground, 264
modulo, 267
class, 354
inheritance, 355
multiple, 356
parameterized, 489
Clear, 382
cmb, 151
coherence, 313, 765
checking, 316
ground, 315
collapse theory, 1022
comm, 141, 171, 179, 187, 1019
comment, 36, 1200
multiline, 1201
commutative, see comm
config, 350, 364, 369, 373
configuration, see config
confluence, 259
connected component, see subsort relation
constant, 70
metarepresentation, 883
qualified, 93
constructor, 194–199
non-free, 196
constructor, see ctor
cont, see continue
continue, 329, 1070
counter, 534–542
cq, see ceq
CRC, 14, 725
crl, 306
ctor, 195, 211
CVC4, 855–864
deadlock freedom, 718
debug, 1062
debug, 1164
debugger, 344, 540, 988–996
debugging, 974, see tracing, term coloring
delay, see vu-narrow, see vu-narrow, see vu-narrow
dependent type, 546
descent function, 878, 900–962
downModule, 905
metaApply, 913
metaCheck, 952
metaDisjointUnify, 923, 926
metFrewrite, 911
metaGetIrredundantVariant, 934
metaGetVariant, 930
metaIrredudantDisjointUnify, 928
metaIrredudantUnify, 927
metaNarrowingApply, 948
metaNarrowingSearch, 946
metaNarrowingSearchPath, 947
metaNormalize, 908
metaParse, 954, 968
metaParseStrategy, 959
metaPrettyPrint, 956
metaPrettyPrintStrategy, 960
metaPrintToString, 958
metaReduce, 907
metaRewrite, 909
metaSrewrite, 918
metaUnify, 921–929
metaVariantDisjointUnify, 937
metaVariantMatch, 945
metaVariantUnify, 936
metaXapply, 914
upModule, 903
upTerm, 904
design, 1–10
Diophantine equation solver, 593
DIRECTORY, 617
directory API, 614–618
distributed dataset, 512
ditto, 213
do clear memo, 231
do clear memo, 1165
dsrew, see dsrewrite
dsrewrite, 712, 1081
metarepresentation, see descent function
early-quit, 1063
ELAN, 20, 154n, 650
eof, 1177
eq, 137
equation, 136–145
executable, 138, 251
metarepresentation, 891
equational condition, 149–167
abbreviated Boolean equation, 152, 158
matching equation, 155, 160, 161
ordinary equation, 157
satisfaction, 159
equational simplification, 258
modulo, 144, 189, 190
sharing, 287n, 289
erew, see erewrite
erewrite, 538, 598, 1069
erewrite-loop-mode, 1047
evaluation strategy, see strategy
ex, see extending
expressiveness, 4–7
extending, 393, 407
external object, 596–648
File IO, 607–612
file.maude, 605–613
filter, see vu-narrow, see vu-narrow, see vu-narrow
filtered variant unify, 809, 1084
finite variant property, 791
checking, 793
fmod, 47, 135
fold, see vu-narrow
format, 205, 421, 986
formula
satisfiable, 858
unsatisfiable, 860
valid, 859
foundations, 11–12
frew, see frewrite
frewrite, 319, 331, 336, 537, 1066
metarepresentation, see descent function
frozen argument, see strategy
frozen, 235
fth, 435
fvu-narrow, 1091
metarepresentation, see descent function
gather, 121, 420
gb, see generated-by
generated-by, 394
get irredundant variants, 796–799
get variants, 795–802, 1086
help, 1037
id, 173, 180, 184, 188, 1020, 1023
idem, 172, 181, 182, 1010–1012, 1021, 1024, 1025
idempotent, see idem
identifier, 38–42, 46, 55, 71, 82, 103
escape character, 40
nonprinting characters, 41
quoted, see quoted identifier
special, 39
identity, see id
in, 24, 32, 34, 1178
inc, see including
including, 395, 412, 413, 452
initial algebra, 164
initial equality, 527–528
interaction, 22–37
interrupt, 342
metarepresentation, see read-eval-print loop
interactive, 1048
internal error, 1013
invariant, 715–716
model checking of, 717–719
bounded, 720–721
irredundant unify, 768, 784
iter, 193, 275, 277, 477, 530, 1033, 1068
iterated, see iter
kind, 78–88
canonical representation, 83
metarepresentation, 880
Kripke structure, 735
associated to a module, 736
label, 241, 300, 701
latex-log, 1049
left id, 174, 176, 185, 1026
linear temporal logic, 732
model checking, see model checking
satisfiability, 745
linear.maude, 594
list
from set, 576–578
generalized, 580–581
of sets, 497
parameterized, 508, 572–573
sorted, 509
sortable, 584–587
strict weak order, 585
total preorder, 586
ll, 1181
load, 25, 35, 1179
loop, 1071
ls, 1180
LTL, see linear temporal logic
LTL+, 748
machine-int.maude, 517
map, 588–589
match, 281, 1073
metarepresentation, see descent function
matching, 257
modulo, 266, 272–278, 314, 1029
with extension, 273, 1030
MAUDE_LIB, 30, 33
mb, 147
membership, 146–148, 1031
metarepresentation, 892
membership equational logic, 134, 510
memo, 229
memoization, 228–233
table size, 230
message, 348
message, 366, 374
metadata, 212, 242, 301, 695, 700
meta-interpreter.maude, 971
MiniMaude, 972–973
Mobile Maude, 624
mod, 49, 299
model checker
implementation, 741
procedure, 740
model checking, 738–744
abstraction, 722–731
logical, 820, 847
model-checker.maude, 734, 737, 742, 743, 747
module, 43–50
algebra, 379
expression, 384, 448, see module operation
functional, 45, 128–293
admissible, 250–252
initial model, 253
mathematical semantics, 130, 133, 143, 163, 165
operational semantics, 132, 142, 269
hierarchy, see module importation
importation, 389–415, 450, 451, 503
extending, 406–408
generated-by, 409–410
implicit, 402
including, 411–414
protecting, 403–405
metarepresentation, 887
object-based, 376
asynchronous, 352
configuration, 349
fairness, 371
synchronous, 353
uniqueness, 351, 370
object-oriented, 346
as system module, 377
dnt, 359, 514
do not transform, 358, 513
object-based-programming, 368
operation, 385
instantiation, 388, 428, 495–507
metarepresentation, 896
renaming, 387, 418–423, 506, 704
summation, 386, 416–417, 505
parameterized, 426, 481–494
bound parameter, 501
free parameter, 502
interface, 482
metarepresentation, 895
parameter, 427, 431
parameter label, 483
parameter theory, 484, 485, 491, 492
predefined, 515–592
signature, 44
extended, see parsing
strategy, 688
importation, 703
parameterized, 705
system, 48, 294–345
admissible, 309
initial model, 325
mathematical semantics, 295, 322
operational semantics, 311, 320
monoid, 446
commutative, 454
monomial, 498
msg, see message
MTT, 13, 724, 727
narrowing, 806, 817–853
completeness, 821–822
folding variant, 807, 818, 846
from multiple initial terms, 850
path commands, 849
with extra variables, 851
with simplification, 823–824
narrowing, 825, 826
no-advise, 1050
no-ansi-color, 1044
no-banner, 1051
no-mixfix, 1052
no-prelude, 1053
no-tecla, 1059
no-wrap, 1054
nonexec, 139, 243, 302, 661, 852
number
floating-point, 551–552
integer, 543–544
machine, 545–547
natural, 529–532
random, 533–541
rational, 548–550
string conversion, 556–558
OBJ, 19, 383, 424
obj, see object
OBJ3, 5n, 6, 18, 219, 380, 486
object, 347
object, 365, 375
op, 65, 87
operation
metalevel, see descent function
partial, 85
total, 86
operator, 64–77, 106
arity, 66
at the kind level, 84, 1035
at the sort level, 1034
built-in, 238, 478, 769
coarity, 68
derived, see view
domain sort, see operator arity
gathering, see parsing
iterated, see iter
mapping, 469, see view, 475
metarepresentation, 890
name
empty syntax, 74
mixfix form, 73
prefix form, 72, 107
several identifiers, 76
overloaded, 90–95, 1015
ad-hoc, 92
subsort, 91, 210
polymorphic, 200, 479
precedence, see parsing
range sort, see operator coarity
ops, 75
optimizing, 976, see debugger, profiler
oth, 437
otherwise, 162, 244–247, 280
overloading, see operator overloaded
owise, see otherwise
parse, 126, 1166
metarepresentation, see descent function
parsing, 113–127
extended grammar, 125
gathering, 119
default pattern, 123
precedence, 114
default value, 122
overridden, 118
path, see vu-narrow
pattern, 156
performance, 8–9, 1004
poly, see polymorphic
polymorphic, 201, 422, 520, 525
polynomial, 499, 500
popd, 1182
pr, see protecting
prec, see precedence
precedence, 117, 419
prelude.maude, 29, 516, 568, 569, 597, 875, 881, 885, 894, 961
preregularity, 109, 1017
modulo, 110
print, 248, 303, 702, 1036
print conceal, 1115
print reveal, 1116
print-to-stderr, 1055
printing
format, 204–209
color, 208
space, 206
metarepresentation, see descent function, see descent function
PRNG, 643
PRNG, 642
PRNG-TEST, 645
PRNG-TEST, 644
probabilistic models, 539
process, 627–647
process.maude, 628
profiler, 999–1003
profiling, 1007
protecting, 392, 404
pushd, 1183
pwd, 1184
Python, 634
q, see quit
qidlist
string conversion, 563–565
quit, 23, 1185
quoted identifier, 559–561
random API, 641
random-api, 646
random-seed, 535, 1056
read-eval-print loop, 970
Real-Time Maude, 17
red, see reduce
reduce, 27, 166, 279, 1064
metarepresentation, see descent function
reflection, 874
moving between levels, see descent function
tower of, 898
resume, 994 (debugger), 1161 (debugger)
rew, see rewrite
rewrite condition, 305–308
rewrite expression, 307
satisfaction, 312
rewrite rule, 296
executable, 310
meaning
computational, 297
logical, 298
metarepresentation, 893
object-oriented, 357
rewrite, 318, 327, 333, 335, 536, 1065
metarepresentation, see descent function
rewriting
modulo, 317
object-oriented, 360
sharing, 288n
rewriting logic
proof equivalence, 324
reflective, 876
rewrite proof, 323
right id, 175, 177, 186, 1027
ring, 459
rl, 304
SAT problem, 861
SAT solver, 862
satisfiability module theories, see SMT
SCC, 16, 198, 726, 729
search
object-oriented, 361
search, 337, 1075
metarepresentation, see descent function
object-oriented, 362
searching, see search
select, 28, 1167
semiring, 455
set
from list, 577–579
generalized, 582–583
parameterized, 574–575
partially ordered, 461
totally ordered, 462
set clear memo, 232
set break, 991, 1158
set clear memo, 1168
set clear module caches, 1169
set clear profile, 1001, 1155
set clear rules, 1072
set extend, 523, 1170
set generate-by, 1171
set include, 1172
set oo include, 1173
set print, 985
set print attribute, 1111
set print attribute newline, 1110
set print color, 1112
set print conceal, 1114
set print constants with sorts, 1113, 1117
set print flattened, 1118
set print format, 1119
set print graph, 1120
set print hooks, 1121
set print label attribute, 1122
set print latex, 1123
set print mixfix, 1124
set print number, 531, 1125
set print parentheses, 1128
set print rat, 549
set print rational, 1126
set print with aliases, 1127
set profile, 1000, 1156
set protect, 522, 1174
set show advisories, 1129
set show breakdown, 1130
set show command, 1131
set show gc, 1132
set show loop stats, 1133
set show loop timing, 1134
set show resources, 1135
set show stats, 1136
set show timing, 1137
set trace, 284, 979, 1008, 1095
set trace body, 1096
set trace builtin, 1097
set trace condition, 1098
set trace eq, 1099
set trace mb, 1100
set trace rewrite, 1101
set trace rl, 1102
set trace sd, 1103
set trace select, 285, 980, 1104
set trace substitution, 1105
set trace whole, 1106
set verbose, 378, 781, 844, 1175
set print format, 207
show frontier states, 839, 1092
show, 290
show all, 1138
show components, 292, 1139
show desugared, 1140
show eqs, 1141
show mbs, 1142
show module, 1143
show modules, 1144
show ops, 1145
show path, 338, 1077
show path labels, 339, 1078
show path states, 340, 1079
show processed view, 1146
show profile, 1002, 1157
show rls, 326, 1147
show sds, 1148
show search graph, 341, 1076
show sorts, 291, 1149
show strats, 1150
show summary, 1151
show vars, 1152
show view, 1153
show views, 1154
show most general states, 848, 1093
show pid, 1057
simplicity, 2–3
sload, 26, 1186
smod, 691
SMT, 854–873
SMT-LIB, 857–872
Core, 867
Ints, 868
Reals, 869
Reals-Ints, 870
smt.maude, 866
socket, 619–626
buffered, 623–625
two-way communication, 621–622
socket.maude, 620
socket.maude, 631
sort, 51–56
error supersort, see kind
least sort, 108, 255
mapping, 467, see view
metarepresentation, 879
name collision, 490
parameterized, 487, 488
structured, 54
sort decreasingness, 262
sort, 52
sorts, 53
special, 237, 518
srew, see srewrite
srewrite, 653, 711, 1080
metarepresentation, see descent function
stack, 493 (Full Maude)
stack overflow, 1014
standard streams, 604–606
Status report, 997–998
step, 993 (debugger), 1162 (debugger)
sth, 707
strat, 223
Stratego, 651
strategy
internal, 963–964
object-message fair, 363–367, 372
operator, 214–227
bottom-up, see eager
default, 222
eager, 216
frozen, 226, 234–236, 321, 827
lazy, 218
operator-by-operator, 217, 221
strategy language, 649–714
all, 660
alternative, 670
amatch, 666
amatchrew, 684, 685
concatenation, 668
conditional, 674
csd, 699
disjunction, 669
fail, 673
idle, 672
iteration, 671
match, 664
matchrew, 682
metarepresentation, 886
named strategies, 690
named strategy
mapping, 709
overloaded, 696
negation, 677
non-void iteration, 676
normalization, 679
not, 678
one, 686
or-else, 675
rule application, 657
initial substitution, 658
rewriting condition, 659
sd, 698
set-theoretic semantics, 656, 667
strat, 693
strategy call, 687
strategy combinator, 652
strategy declaration, 692
strategy definition, 697
strategy expression, 654
strategy module, see module strategy
subject sort, 694
test, 663
test, 681
top, 662
try, 680
xmatch, 665
xmatchrew, 683
strategy, see strat
string, 553–554
number conversion, 555–557
qidlist conversion, 562–564
submodule, 390, see module importation
subsort relation, 57–63
connected component, 61
metarepresentation, 889
partial order, 60
subsort, 58
subsorts, 59
substitution, 254
well-sorted, 256
sufficient completeness, 197
supermodule, 400, see module importation
symbolic reachability analysis, 819, 845
tautology checker, 746
tecla, 1058
term, 105–112
canonical form, 131, 261
relative to strategy, 224
coloring, 984–987
error, 80
flattened, 274
ground, 111, 129
metarepresentation, 882
qualified, 94
undefined, 81
termination, 260
context-sensitive, 270
ground, 265
modulo, 268
th, 436
theory, 425, 430–463
flat, 456, 458n
functional, 432
admissible, 438
mathematical semantics, 439
operational semantics, 440
importation, 447
including, 453, 460
metarepresentation, 888
object-oriented, 434, 464
mathematical semantics, 442
parameter constant, 445
predefined, 566–570
strategy, 706
structured, see theory importation
system, 433
admissible, 444
mathematical semantics, 441
operational semantics, 443
TIME, 637
time API, 636
time-api, 640
TIME-INTERVAL, 639
TIME-UTC-LOCAL, 638
token, 967, 1199
trace deselect, 1109
trace exclude, 982
trace include, 1107
trace select, 286, 981, 1108
tracing, 978–983, 1005
trust, 603, 609, 611, 616, 630, 633, 635, 1060
unification, 749–786
-unification, 751
algorithm, 763
associative, 780–782
associative-commutative, 772–773
associative-commutative-identity, 776–777
associative-identity, 783
equational, 752
finitary, 761
hybrid approach, 764
identity, 778–779
iter, 774–775
order-sorted, 757–766
problem, 758
semantic, 753
syntactic, 750
unitary, 762
variant-based, 804–815
unifier, 754
-unifier, 759
complete set, 760
most general, 755
semantic, 756
unify, 767–785, 1082
metarepresentation, see descent function
universal theory, 877
Universal, 203, 521, 524
var, 100
in views, 473
variable, 96–104
fresh, 770, 771, 797, 798, 924, 925, 932, 933, 940, 949
in a module, 99, 101
metarepresentation, 884
on-the-fly, 97, 98
variant, 787–816
based unification, 805–814
incremental, 811
with irreducibility constraints, 810, 939
complete set, 789
finite variant property, 792
generation, 794–803
incremental, 801
with irreducibility constraints, 800, 931, 935
variant, 790
variant match, 812–1085
variant unify, 808–813, 1083
metarepresentation, see descent function
vars, 102
vector, 595
version, 1038
vfold, see vu-narrow
view, 429, 465–480, 708
between theories, 474, 710
metarepresentation, 897, 899
object-oriented, 471
parameterized, 511
predefined, 567–571
view, 466
vu-narrow, 828, 1087
delay, 833, 841, 942, 1090
filter, 832, 840, 941, 1089
fold, 829, 1088
metarepresentation, see descent function
path, 831
vfold, 830
where, 992 (debugger), 1163 (debugger)
xmatch, 276, 282, 283, 1074
metarepresentation, see descent function
xml-log, 1061