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