Cairn
Docs
Claims
Blog
Packages
Claims · pairs
pairs 0.1.3: claims
Everything pairs 0.1.3 claims a person can do and see, and what holds, by place, each with its evidence.
22 proved3 no proof
Pairs window pairs^1
The game's window: the pack's name and the counters, the cards in a grid, the field to open a pack from a folder or an https URL, and New Game; when the game is won, the result and New Game in place of the grid.
Moves
| Id | Claim | Reads as |
|---|---|---|
pairs^2 | Turn a cardClick a face-down card. | proved |
pairs^3 | New GamePress New Game. | proved |
pairs^4 | Open a packType a folder (/… or ~/…) or an https:// URL into the pack field, and press Enter. | proved |
pairs^5 | Cancel loadingWhile a pack is loading, press Cancel. | proved |
Flows
| Id | Claim | Reads as |
|---|---|---|
pairs^30 | Find a pairTurn two cards with the same face. | proved |
pairs^31 | A mismatchTurn two cards with different faces. | proved |
pairs^32 | Win a gameTurn the cards of each face in turn, a pair at a time. | proved |
Pairs menu pairs^6
The menu of Pairs's menu bar item: New Game, the Packs submenu and Open Packs Folder.
Moves
| Id | Claim | Reads as |
|---|---|---|
pairs^8 | Open the menuClick Pairs's menu bar item. | proved |
pairs^9 | New GameChoose New Game. | proved |
pairs^12 | Open Packs FolderChoose Open Packs Folder. | proved |
Packs submenu pairs^7
The packs Pairs can open: the bundled ones, then each folder in the packs folder; the pack being played is checked.
Moves
| Id | Claim | Reads as |
|---|---|---|
pairs^10 | A bundled packChoose a bundled pack (Shapes, Patterns) in the Packs submenu. | proved |
pairs^11 | A pack in the packs folderChoose a pack listed from the packs folder (~/Library/Application Support/Pairs/Packs) in the Packs submenu. | proved |
Invariants
What holds in every state the app can reach.
| Id | Claim | Reads as |
|---|---|---|
pairs^20 | The board is a deal of the packThe game deals the pack's number of pairs, from distinct faces of the pack; the cards are those faces, each on exactly two cards, in an order the clock's seed shuffled. | proved |
pairs^21 | At most two unmatched cards face upAt most two cards are face up and unmatched at any time: turning a third turns the mismatched two back first. | proved |
pairs^22 | Won exactly when every card is matchedThe game is won, and its time recorded, exactly when every card on the board is matched. | proved |
pairs^23 | The game can always be wonFrom every state the app reaches, some sequence of cards to turn wins the game: the cards of every face not yet matched, a pair at a time (Game.solve). | proved |
pairs^24 | Moves count pairs turnedThe move counter is the number of pairs of cards turned this game: half the cards turned, rounded down. | proved |
pairs^25 | A matched card stays matchedOnce a pair is matched it stays matched, face up, until a new game is dealt; nothing the person clicks and nothing the host answers turns it back. | proved |
pairs^26 | Best scores only improveA pack's best moves and best time only ever get better: a win records the better of each, and scores read from disk are merged the same way, never overwriting a better one. | proved |
pairs^27 | No request is lostEvery request Pairs makes (manifests, images, the scores file, the packs folder) is answered, cancelled or still awaited, exactly once; ids awaited are distinct and were issued. Cairn's runtime sends at most six network requests at a time and drops replies to cancelled ones. | proved |
pairs^28 | A late reply changes nothingA reply to a request Pairs isn't waiting for (cancelled when a pack switch stopped it, superseded, or a duplicate) leaves everything as it was. | proved |
pairs^29 | Only a finished pack changes the boardA reply changes the board only when it is an image answering ready, to a request the pack being loaded made since it began loading: a failure, a pack.json that doesn't parse, a reply for a pack that was switched away from, or any reply while no pack is loading leaves the game as it was. | proved |