| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 16 kB |
|
Quellcode-Bibliothek XOTests.vdmsl Sprache: VDM |
|||||||||
|
--
-- A simple model of a tic-tac-toe game (noughts and crosses) -- module XOTests imports from XO operations play types Pos renamed Pos; PlayOrder renamed PlayOrder; Moves renamed Moves; Player renamed Player values SIZE renamed SIZE exports all definitions -- Test data and supporting operations/traces values OX = [<NOUGHT>, <CROSS>]; XO = [<CROSS>, <NOUGHT>]; XX = [<CROSS>]; T1 = [mk_Pos(1,1), mk_Pos(1,2), mk_Pos(2,1), mk_Pos(1,3), mk_Pos(3,1)]; T2 = [mk_Pos(1,1), mk_Pos(1,2), mk_Pos(1,3), mk_Pos(2,2), mk_Pos(3,1), mk_Pos(3,2)]; E1 = [mk_Pos(1,1), mk_Pos(1,1), mk_Pos(1,2), mk_Pos(2,1), mk_Pos(1,3)]; S = {1, ..., SIZE} operations test: PlayOrder * Moves ==> Player | <DRAW> | <UNFINISHED> test(playorder, moves) == XO`play(playorder, moves); traces ALL: let ALLPOS = { mk_Pos(r, c) | r, c in set S } in -- All 3x3 = 9 positions let m1 in set ALLPOS in -- 9 1st moves let m2 in set ALLPOS \ {m1} in -- 72 1st-2nd pairs let m3 in set ALLPOS \ {m1, m2} in -- 504 1st-2nd-3rd etc... let m4 in set ALLPOS \ {m1, m2, m3} in -- 3024 let m5 in set ALLPOS \ {m1, m2, m3, m4} in -- 15120 (minimum) -- let m6 in set ALLPOS \ {m1, m2, m3, m4, m5} in -- 60480 -- let m7 in set ALLPOS \ {m1, m2, m3, m4, m5, m6} in -- 181440 -- let m8 in set ALLPOS \ {m1, m2, m3, m4, m5, m6, m7} in -- 362880 -- let m9 in set ALLPOS \ {m1, m2, m3, m4, m5, m6, m7, m8} in -- 362880 XO`play(XO, [m1, m2, m3, m4, m5]); end XOTests ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
