562:
bypassed, forcing the state machine into the distant state. This allows all (abstract) states to be covered quickly during testing. Output distinguishability is the key property supporting the scalable testing method. It allows the tester to treat the processing functions φ as simple labels, whose detailed behaviour may be safely ignored, while testing the state machine of the next integration layer. The unique outputs are witness values, which guarantee that a particular function was invoked.
1296:
454:. In this case, the input, memory and output types for the low-level machines will be different from those defined for the high-level machine. Either, this is treated as an expansion of the data sets used at the high level, or there is a translation from more abstract data sets at the high level into more detailed data sets at the lower level. For example, a command
911:. This is the smallest set of test sequences that reaches every state and then attempts every possible transition once, from that state. Now, the input alphabet consists of (the labels of) every function φ in Φ. Let us construct a set of length-1 test sequences, consisting of single functions chosen from Φ, and call this Φ
35:
model of computation. Using this methodology, it is likely to identify a finite test-set that exhaustively determines whether the tested system's implementation matches its specification. This goal is achieved by a divide-and-conquer approach, in which the design is decomposed by refinement into a
557:
A minimal machine is the machine with the fewest states and transitions for some given behaviour. Keeping the specification minimal simply ensures that the test sets are as small as possible. A deterministic machine is required for systems that are predictable. Otherwise, an implementation could
152:
This supports a divide-and-conquer approach, in which the overall system architecture is specified first, then each major system operation is specified next, followed by subroutines, and so forth. At each step, the level of complexity is manageable, because of the independence of each layer. In
561:
Test completeness is needed to ensure that the implementation is testable within tractable time. For example, if a system has distant, or hard-to-reach states that are only entered after memory has reached a certain limiting value, then special test inputs should be added to allow memory to be
108:
This level of testing can be difficult to achieve, since software systems are extremely complex, with hundreds of thousands of states and millions of transitions. What is needed is a way of breaking down the specification and testing problem into parts which can be addressed separately.
1261:
545:: It must be possible to distinguish which processing function was invoked from its output value alone, for all memory-input pairs. This ensures that the state machine can be decoupled from the processing functions. To ensure output distinguishability, the
881:
51:
principles are followed during specification and implementation. The resulting scalability means that practical software and hardware systems consisting of hundreds of thousands of states and millions of transitions have been tested successfully.
531:: Each processing function φ must be executable for at least one input, with respect to all memory states. This ensures that there are no deadlocks, where the machine is blocked by the current state of memory. To ensure test completeness, the
484:
Systems are otherwise specified down to the level at which the designer is prepared to trust the primitive operations supported by the implementation environment. It is also possible to test small units exhaustively by other testing methods.
320:
describing the main user interaction with the system. For example, the word processor will exist in a number of states, in which keystrokes and commands will have different effects. Suppose that this word processor exists in the states
64:
is merely hopeful, seeking to exercise the software system in various ways to see whether any faults can be detected. Testing may indeed reveal some faults, but can never guarantee that the system is correct, once testing is over.
1114:
1036:
601:
To test all behaviours, it must be possible to drive a machine into all of its states, then attempt all possible transitions (those which should succeed, and those which should be blocked) to achieve full
642:
The basis for the test generation strategy is Tsun S. Chow's W-Method for testing finite-state automata, chosen because it supports the testing of redundant implementations. Chow's method assumes simple
415:. This recognises that every interaction could be a simple character insertion, a menu command or a cursor placement. Any given interaction is a 3-tuple, but some places may be empty. For example, (
1171:
236:
at each step. For each input, the machine takes one step, producing an output, such that input/output pairs may be matched exactly. This contrasts with other approaches in which the system
958:
40:, which are implemented as separate modules, then tested bottom-up. At each integration stage, the testing method guarantees that the tested components are correctly integrated.
260:
When following the (Stream) X-Machine methodology, the first stage is to identify the various types of data to be processed. For example, a word processor will use basic types
794:
515:. This means that the state machine should not contain redundant states, that is, states in which the observable transition behaviour is identical to that in some other state.
725:
745:
450:. The most common kind of refinement is to take each of the major processing functions (which were the labels on the high-level machine) and treat these as separate
558:
make an arbitrary choice regarding which transition was taken. Some recent work has relaxed this assumption to allow testing of non-deterministic machines.
376:
defined above. This treats a document as a text string, with two positions marking a possible selection and a flag to indicate modification since the last
963:
This will attempt every possible transition from every state. For those which succeed, we must validate the destination states. So, the smallest test-set
369:
state, when any menu command has finished. This state machine is designed and labelled informally with the various actions that cause it to change state.
655:
are treated simply as labels (inputs, in Chow's terms) and the distinguishing outputs are used directly. (Later, a mapping from real inputs and memory (
372:
The input, memory and output types for the top-level machine are now formalised. Suppose that the memory type of the simple word processor is the type
481:, in which a simple state-space is partitioned into a more complex state-space. Ipate proves these two kinds of refinement to be eventually equivalent
1044:
1414:
K. Bogdanov and M. Holcombe (1998) 'Automated test set generation for
Statecharts', in: D. Hutter, W Stephan, P. Traverso and M. Ullmann eds.
44:
977:
225:, that is, they consume one input from the input stream, possibly modify memory, and produce one output on the output stream (see the
1364:
693:, the smallest set of test sequences that reaches every state. This can be constructed by automatic breadth-first exploration of
570:
The (Stream) X-Machine
Testing Method assumes that both the design and the implementation can be considered as (a collection of)
173:, as the basis for the testing method. The advantage of this variant was the way in which testing could be controlled. In a
1518:
1256:{\displaystyle T_{\mathrm {k} }::=C\otimes \left(\Phi _{0}\cup \Phi _{1}\ldots \cup \Phi _{\mathrm {k} }\right)\otimes W}
427:, ε, 32) would mean selecting the text between the current cursor position and the place between characters 32 and 33.
365:
state. In these states, certain keystrokes may have different meanings. The word processor eventually returns to the
93:
methods exploit the specification systematically, generating test-sets which exercise the implemented software system
647:
with observable inputs and outputs, but no directly observable states. To map onto Chow's formalism, the functions φ
252:. Powerful methods exist for testing systems that conform to finite-state specifications, such as Chow's W-method.
525:
for the current memory and next input value. This ensures that the required behaviour to be tested is predictable.
1523:
918:
125:
model as the basis for software specification in the late 1980s. This is because the model cleanly separates the
1501:
Words, Sequences, Grammars, Languages: Where
Biology, Computer Science, Linguistics and Mathematics Meet, Vol II
610:
testing (see above). For transitions which succeed, the destination state must also be verified. Note that if
380:-command. A more complex word processor might support undoable editing, with a sequence of document states:
73:
describing the intended behaviour of the system, against which the implementation is later tested (a kind of
618:
have the same number of states, the above describes the smallest test-set that achieves the objective. If
876:{\displaystyle C\otimes W=\{\langle ac\rangle ,\langle ad\rangle ,\langle bc\rangle ,\langle bd\rangle \}}
1139:, the above test-set may not be sufficient to guarantee the conformant behaviour of replicated states in
1382:
F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'.
644:
532:
512:
249:
154:
134:
86:
70:
1398:
F. Ipate and M. Holcombe (1997) 'An integration testing method that is proved to find all faults',
74:
133:
carried out by the system. At a given level of abstraction, the system can be viewed as a simple
434:
processing function was executed, in response to a given input. This relates to the property of
90:
78:
66:
24:
704:
430:
The output type for the machine is designed so that it is possible to determine from the output
730:
248:
about the details of the processing functions and consider the (sub-)system just as a simple
137:
consisting of a few states and transitions. The more complex processing is delegated to the
652:
571:
522:
498:
451:
447:
317:
241:
226:
206:
174:
170:
118:
61:
37:
32:
28:
1283:=3 is quite exhaustive, revealing all state-related faults in really poor implementations.
1368:
682:
should yield at least one observable difference, compared to starting in any other state.
494:
308:(the text, a possible selection, and a flag to signal if the document has been modified).
145:. Later, each processing function may be separately exposed and characterized by another
48:
1361:
1143:. So, sets of longer test sequences are chosen, consisting of all pairs of functions Φ
477:, in which the behaviour of the processing functions is elaborated in more detail, and
1295:
104:
Full negative testing: confirms that no unintended behaviour is present in the system.
1512:
521:: For each state of the machine, at most one of the processing functions φ should be
101:
Full positive testing: confirms that all desired behaviour is present in the system;
1447:
M. Holcombe (1988) 'X-machines as a basis for dynamic system specification',
1466:
T. S. Chow (1978) 'Testing software design modelled by finite state machines',
674:, the smallest set of test sequences that uniquely characterizes each state in
77:). The specification can be validated against the user-requirements and later
1109:{\displaystyle T_{1}::=C\otimes \left(\Phi _{0}\cup \Phi _{1}\right)\otimes W}
240:(taking multiple steps) before any observation is made. Furthermore, layered
82:
1499:
F. Ipate and M. Holcombe (2000) 'Testing non-deterministic X-machines'. In:
594:
need not be a minimal machine - it may have more states and transitions than
493:
The (Stream) X-Machine methodology requires the designer to observe certain
446:
If a system is complex, then it will most likely be decomposed into several
232:
The benefits for testing are that software systems designed in this way are
166:
146:
122:
89:
by mathematical reasoning (eliminating any logical design flaws). Complete
423:, ε, 32) would mean placing the cursor between characters 32 and 33; and (
353:
is held down. Once the selection is established, it should return to the
546:
497:
conditions. These are typically not too difficult to satisfy. For each
97:, to determine whether it conforms to the specification. In particular:
678:. That is, when starting in a given state, exercising the sequences in
272:(mouse or menu command). There may be other constructed types, such as
1271:
in which chains of duplicated states are expected to be no longer than
1490:, PhD Thesis, Department of Computer Science, University of Sheffield.
586:, the machine of the implementation, exactly matches the behaviour of
141:
on the transitions, which modify the underlying fundamental data type
153:
particular, it is easy for software engineers to validate the simple
357:
state. Likewise, if a menu option is chosen, this should enter the
1488:
Theory of X-Machines with
Applications in Specification and Testing
582:), the purpose of testing is to determine whether the behaviour of
1267:
This test-set completely validates the behaviour of a non-minimal
1031:{\displaystyle T_{1}::=C\otimes W\cup C\otimes \Phi _{1}\otimes W}
663:) is chosen to trigger each function φ, according to its domain).
473:
Ipate and
Holcombe mention several kinds of refinement, including
1358:
The Theory and
Practice of Specification Based Software Testing
244:
offer a convenient abstraction. At each level, the tester may
1290:
697:. The test-set which validates all the states of a minimal
419:, 'a', ε) would represent typing the character 'a'; while (
69:
methods seek to improve on this situation, by developing a
31:
and hardware testing that exploits the scalability of the
458:
at the high level could be decomposed into three events:
337:}. We expect the word processor to start in the initial
1306:
1161:
cannot contain chains of duplicated states longer than
1342:
Correct
Systems - Building a Business Process Solution
970:
which completely validates the behaviour of a minimal
209:
are labelled with processing functions of the form φ:
1174:
1047:
980:
921:
797:
733:
707:
626:, longer test sequences are needed to guarantee that
392:)*, which are collapsed to one document every time a
177:, the fundamental data type has a particular form:
165:
Gilbert
Laycock first proposed a particular kind of
149:, modelling the behaviour of that system operation.
1255:
1108:
1030:
952:
875:
739:
719:
399:Suppose that the input type for the machine is:
1275:-1. For most practical purposes, testing up to
891:The above test-set determines whether a minimal
1436:Complete Functional Testing of Hardware Designs
590:, the machine of the specification. Note that
205:is the internal memory. The transitions of a
1400:International Journal of Computer Mathematics
549:of a function φ may be extended with special
8:
1503:, eds. C Martin-Vide and V. Mitrana, Kluwer.
870:
867:
858:
852:
843:
837:
828:
822:
813:
810:
574:. For each pair of corresponding machines (
953:{\displaystyle K:=C\cup C\otimes \Phi _{1}}
1124:is the set containing the empty sequence {
903:also has the same transition behaviour as
1468:IEEE Transactions on Software Engineering
1378:
1376:
1336:
1334:
1235:
1234:
1218:
1205:
1180:
1179:
1173:
1165:-1. The final test formula is given by:
1089:
1076:
1052:
1046:
1016:
985:
979:
944:
920:
796:
732:
706:
292:(the start and end of the selection) and
1462:
1460:
1360:. PhD Thesis, University of Sheffield.
1352:
1350:
1344:. Springer, Applied Computing Series.
1330:
1438:, PhD Thesis, University of Sheffield.
1038:. This formula can be rearranged as:
915:. The transition cover is defined as
598:and still behave in an identical way.
553:that are only relevant during testing.
501:in the specification, we must obtain:
47:limitations by requiring that certain
18:(Stream) X-Machine Testing Methodology
622:has more states and transitions than
161:Incrementally Testable Specifications
7:
1416:Applied Formal Methods: FM-Trends 98
1157:, when the tester is satisfied that
117:Mike Holcombe first proposed using
1236:
1231:
1215:
1202:
1181:
1086:
1073:
1013:
941:
899:. To determine whether a minimal
751:of the two sets. For example, if
539:that are only used during testing.
14:
1420:Lecture Notes in Computer Science
316:The top-level specification is a
113:Scalable, Abstract Specifications
43:The methodology overcomes formal
1340:M. Holcombe and F. Ipate (1998)
1294:
685:To reach each state expected in
666:To identify specific states in
535:φ may be extended with special
508:: The specification must be a
280:* (a sequence of characters),
1:
345:state if either the mouse is
1449:Software Engineering Journal
1147:, all triples of functions Φ
907:, the tester constructs the
689:, the tester constructs the
268:(mouse cursor position) and
519:Deterministic Specification
201:* is an output stream, and
157:against user requirements.
1540:
720:{\displaystyle C\otimes W}
651:on the transitions of the
489:Design-For-Test Conditions
341:state, but to move to the
1367:November 5, 2007, at the
634:also behave as expected.
543:Output Distinguishability
436:output distinguishability
740:{\displaystyle \otimes }
312:High-Level Specification
1486:Florentin Ipate (1995)
1356:Gilbert Laycock (1993)
895:has the same states as
887:Testing all Transitions
672:characterization set, W
442:Low-Level Specification
396:-command is performed.
1303:This section is empty.
1257:
1110:
1032:
954:
877:
741:
721:
197:* is an input stream,
1519:Theory of computation
1258:
1135:has more states than
1111:
1033:
955:
878:
742:
722:
645:finite-state machines
506:Minimal Specification
475:functional refinement
155:finite-state machines
129:of a system from the
1434:Salim Vanak (2001),
1418:, Boppard, Germany,
1172:
1045:
978:
919:
795:
749:concatenated product
731:
705:
533:domain of a function
513:finite-state machine
470:at the lower level.
256:Specification Method
250:finite-state machine
139:processing functions
135:finite-state machine
71:formal specification
1384:Int. J. Comp. Math.
909:transition cover, K
438:, described below.
229:for more details).
75:conformance testing
1253:
1151:up to some limit Φ
1106:
1028:
950:
873:
737:
717:
638:Testing all States
264:(keyboard input),
238:runs to completion
227:associated article
91:functional testing
67:Functional testing
25:functional testing
1323:
1322:
670:, Chow chooses a
653:Stream X-Machines
572:Stream X-Machines
529:Test Completeness
452:Stream X-Machines
448:Stream X-Machines
242:Stream X-Machines
38:Stream X-Machines
1531:
1524:Software testing
1504:
1497:
1491:
1484:
1478:
1464:
1455:
1445:
1439:
1432:
1426:
1412:
1406:
1396:
1390:
1380:
1371:
1354:
1345:
1338:
1318:
1315:
1305:You can help by
1298:
1291:
1262:
1260:
1259:
1254:
1246:
1242:
1241:
1240:
1239:
1223:
1222:
1210:
1209:
1186:
1185:
1184:
1127:
1126:⟨⟩
1115:
1113:
1112:
1107:
1099:
1095:
1094:
1093:
1081:
1080:
1057:
1056:
1037:
1035:
1034:
1029:
1021:
1020:
990:
989:
959:
957:
956:
951:
949:
948:
882:
880:
879:
874:
790:
782:
770:
762:
746:
744:
743:
738:
726:
724:
723:
718:
499:Stream X-Machine
479:state refinement
318:Stream X-Machine
207:Stream X-Machine
175:Stream X-Machine
171:Stream X-Machine
119:Samuel Eilenberg
62:software testing
33:Stream X-Machine
1539:
1538:
1534:
1533:
1532:
1530:
1529:
1528:
1509:
1508:
1507:
1498:
1494:
1485:
1481:
1465:
1458:
1454:(2), pp. 69–76.
1446:
1442:
1433:
1429:
1413:
1409:
1397:
1393:
1381:
1374:
1369:Wayback Machine
1355:
1348:
1339:
1332:
1328:
1319:
1313:
1310:
1289:
1230:
1214:
1201:
1200:
1196:
1175:
1170:
1169:
1156:
1150:
1146:
1125:
1123:
1085:
1072:
1071:
1067:
1048:
1043:
1042:
1012:
981:
976:
975:
969:
940:
917:
916:
914:
889:
793:
792:
784:
776:
764:
756:
729:
728:
703:
702:
650:
640:
568:
495:design for test
491:
444:
314:
258:
163:
121:'s theoretical
115:
58:
49:design for test
12:
11:
5:
1537:
1535:
1527:
1526:
1521:
1511:
1510:
1506:
1505:
1492:
1479:
1477:, pp. 178–187.
1456:
1440:
1427:
1425:, pp. 107–121.
1407:
1405:, pp. 159–178.
1391:
1389:, pp. 197–219.
1372:
1346:
1329:
1327:
1324:
1321:
1320:
1301:
1299:
1288:
1285:
1265:
1264:
1252:
1249:
1245:
1238:
1233:
1229:
1226:
1221:
1217:
1213:
1208:
1204:
1199:
1195:
1192:
1189:
1183:
1178:
1152:
1148:
1144:
1121:
1118:
1117:
1105:
1102:
1098:
1092:
1088:
1084:
1079:
1075:
1070:
1066:
1063:
1060:
1055:
1051:
1027:
1024:
1019:
1015:
1011:
1008:
1005:
1002:
999:
996:
993:
988:
984:
974:is given by:
967:
947:
943:
939:
936:
933:
930:
927:
924:
912:
888:
885:
872:
869:
866:
863:
860:
857:
854:
851:
848:
845:
842:
839:
836:
833:
830:
827:
824:
821:
818:
815:
812:
809:
806:
803:
800:
736:
716:
713:
710:
691:state cover, C
648:
639:
636:
567:
566:Testing Method
564:
555:
554:
540:
526:
516:
490:
487:
443:
440:
313:
310:
257:
254:
162:
159:
114:
111:
106:
105:
102:
57:
54:
45:undecidability
36:collection of
13:
10:
9:
6:
4:
3:
2:
1536:
1525:
1522:
1520:
1517:
1516:
1514:
1502:
1496:
1493:
1489:
1483:
1480:
1476:
1473:
1469:
1463:
1461:
1457:
1453:
1450:
1444:
1441:
1437:
1431:
1428:
1424:
1421:
1417:
1411:
1408:
1404:
1401:
1395:
1392:
1388:
1385:
1379:
1377:
1373:
1370:
1366:
1363:
1359:
1353:
1351:
1347:
1343:
1337:
1335:
1331:
1325:
1317:
1308:
1304:
1300:
1297:
1293:
1292:
1286:
1284:
1282:
1278:
1274:
1270:
1250:
1247:
1243:
1227:
1224:
1219:
1211:
1206:
1197:
1193:
1190:
1187:
1176:
1168:
1167:
1166:
1164:
1160:
1155:
1142:
1138:
1134:
1129:
1103:
1100:
1096:
1090:
1082:
1077:
1068:
1064:
1061:
1058:
1053:
1049:
1041:
1040:
1039:
1025:
1022:
1017:
1009:
1006:
1003:
1000:
997:
994:
991:
986:
982:
973:
966:
961:
945:
937:
934:
931:
928:
925:
922:
910:
906:
902:
898:
894:
886:
884:
864:
861:
855:
849:
846:
840:
834:
831:
825:
819:
816:
807:
804:
801:
798:
788:
780:
774:
768:
760:
754:
750:
734:
714:
711:
708:
700:
696:
692:
688:
683:
681:
677:
673:
669:
664:
662:
658:
654:
646:
637:
635:
633:
629:
625:
621:
617:
613:
609:
605:
599:
597:
593:
589:
585:
581:
577:
573:
565:
563:
559:
552:
548:
544:
541:
538:
534:
530:
527:
524:
520:
517:
514:
511:
507:
504:
503:
502:
500:
496:
488:
486:
482:
480:
476:
471:
469:
465:
461:
457:
453:
449:
441:
439:
437:
433:
428:
426:
422:
418:
414:
410:
406:
402:
397:
395:
391:
387:
383:
379:
375:
370:
368:
364:
360:
356:
352:
348:
344:
340:
336:
332:
328:
324:
319:
311:
309:
307:
303:
299:
295:
291:
287:
283:
279:
275:
271:
267:
263:
255:
253:
251:
247:
243:
239:
235:
230:
228:
224:
220:
216:
212:
208:
204:
200:
196:
192:
188:
184:
180:
176:
172:
168:
160:
158:
156:
150:
148:
144:
140:
136:
132:
128:
124:
120:
112:
110:
103:
100:
99:
98:
96:
92:
88:
84:
80:
76:
72:
68:
63:
55:
53:
50:
46:
41:
39:
34:
30:
26:
23:
19:
1500:
1495:
1487:
1482:
1474:
1471:
1467:
1451:
1448:
1443:
1435:
1430:
1422:
1419:
1415:
1410:
1402:
1399:
1394:
1386:
1383:
1357:
1341:
1311:
1307:adding to it
1302:
1287:Applications
1280:
1276:
1272:
1268:
1266:
1162:
1158:
1153:
1140:
1136:
1132:
1130:
1119:
971:
964:
962:
908:
904:
900:
896:
892:
890:
786:
778:
772:
766:
758:
752:
748:
747:denotes the
698:
694:
690:
686:
684:
679:
675:
671:
667:
665:
660:
656:
641:
631:
627:
623:
619:
615:
611:
607:
603:
600:
595:
591:
587:
583:
579:
575:
569:
560:
556:
551:test outputs
550:
542:
536:
528:
518:
509:
505:
492:
483:
478:
474:
472:
467:
463:
459:
455:
445:
435:
431:
429:
424:
420:
416:
412:
408:
404:
400:
398:
393:
389:
385:
381:
377:
373:
371:
366:
362:
358:
354:
350:
346:
342:
338:
334:
330:
326:
322:
315:
305:
301:
297:
293:
289:
285:
281:
277:
273:
269:
265:
261:
259:
245:
237:
233:
231:
222:
218:
214:
210:
202:
198:
194:
190:
186:
182:
178:
164:
151:
142:
138:
130:
127:control flow
126:
116:
107:
95:exhaustively
94:
59:
42:
27:approach to
21:
17:
15:
537:test inputs
384: ::= (
1513:Categories
1326:References
630:states in
403: ::=
296: ::=
284: ::=
276: ::=
234:observable
131:processing
83:consistent
56:Motivation
1314:July 2010
1248:⊗
1232:Φ
1228:∪
1225:…
1216:Φ
1212:∪
1203:Φ
1194:⊗
1101:⊗
1087:Φ
1083:∪
1074:Φ
1065:⊗
1023:⊗
1014:Φ
1010:⊗
1004:∪
998:⊗
942:Φ
938:⊗
932:∪
868:⟩
859:⟨
853:⟩
844:⟨
838:⟩
829:⟨
823:⟩
814:⟨
802:⊗
735:⊗
712:⊗
701:is then:
628:redundant
464:MouseMove
460:MouseDown
409:Character
390:Selection
351:shift-key
349:, or the
343:Selecting
327:Selecting
302:Selection
282:Selection
278:Character
262:Character
193:*, where
167:X-machine
147:X-machine
123:X-machine
29:software-
1365:Archived
1362:Abstract
791:}, then
789:⟩
785:⟨
781:⟩
777:⟨
769:⟩
765:⟨
761:⟩
757:⟨
727:, where
608:negative
604:positive
547:codomain
421:Position
413:Position
382:Document
374:Document
294:Document
290:Position
286:Position
266:Position
87:complete
22:complete
1279:=2, or
1120:where Φ
523:enabled
510:minimal
468:MouseUp
405:Command
367:Writing
359:Editing
355:Writing
347:dragged
339:Writing
335:Editing
323:Writing
306:Boolean
270:Command
771:} and
456:Select
425:Select
417:Insert
363:Filing
331:Filing
246:forget
169:, the
81:to be
79:proven
432:which
60:Much
20:is a
1423:1641
1137:Spec
905:Spec
897:Spec
695:Spec
687:Spec
676:Spec
624:Spec
614:and
612:Spec
606:and
596:Spec
588:Spec
576:Spec
394:save
386:Text
378:save
298:Text
274:Text
185:* ×
85:and
16:The
1475:(3)
1309:.
1269:Imp
1188:::=
1159:Imp
1141:Imp
1133:Imp
1131:If
1128:}.
1059:::=
992:::=
972:Imp
901:Imp
893:Imp
775:= {
755:= {
699:Imp
668:Imp
657:mem
632:Imp
620:Imp
616:Imp
592:Imp
584:Imp
580:Imp
361:or
223:Mem
219:Out
211:Mem
203:Mem
199:Out
187:Mem
183:Out
1515::
1470:,
1459:^
1403:63
1387:68
1375:^
1349:^
1333:^
960:.
926::=
883:.
783:,
763:,
661:in
659:,
578:,
466:,
462:,
411:×
407:×
401:In
388:×
333:,
329:,
325:,
304:×
300:×
288:×
221:×
217:→
215:In
213:×
195:In
191:In
189:×
181:=
1472:4
1452:3
1316:)
1312:(
1281:k
1277:k
1273:k
1263:.
1251:W
1244:)
1237:k
1220:1
1207:0
1198:(
1191:C
1182:k
1177:T
1163:k
1154:k
1149:3
1145:2
1122:0
1116:,
1104:W
1097:)
1091:1
1078:0
1069:(
1062:C
1054:1
1050:T
1026:W
1018:1
1007:C
1001:W
995:C
987:1
983:T
968:1
965:T
946:1
935:C
929:C
923:K
913:1
871:}
865:d
862:b
856:,
850:c
847:b
841:,
835:d
832:a
826:,
820:c
817:a
811:{
808:=
805:W
799:C
787:d
779:c
773:W
767:b
759:a
753:C
715:W
709:C
680:W
649:i
321:{
179:X
143:X
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.