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