Five chess fanatics always manage to fit in a round-robin before their train reaches Waterloo. Yesterday there were no ties in the final order (2 points for win, 1 for draw, 0 for loss). Alapin won his game against the only person who took a game off Bird. Catalan was the only person to lose a game against the financier, who was the only person to lose a game to Dunst. Alapin finished below the ghost-writer. The interpreter scored only 1 point total. The journalist fared worse than the hairdresser. As for Evans, you can work that out for yourself. What is each person’s score and occupation?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
abstract module Group { | |
type T(==) | |
const elems : set<T> | |
function identity(): (r: T) | |
ensures r in elems | |
ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a | |
function compose(a: T, b: T): (r: T) | |
requires a in elems && b in elems | |
ensures r in elems | |
function inverse(a: T) : (r: T) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class Heap { | |
var arr: array<int> | |
constructor Heap (input: array<int>) | |
ensures this.arr == input { | |
this.arr := input; | |
} | |
function parent(idx: int): int | |
{ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
least predicate perm<T(!new)>(p: seq<T>, q: seq<T>) | |
{ | |
|| (p == [] && q == []) | |
|| (exists x: T, m: seq<T>, n: seq<T> :: p == [x] + m && q == [x] + n && perm(m, n)) | |
|| (exists x: T, y: T, m: seq<T> :: p == [x, y] + m && q == [y, x] + m) | |
|| (exists m: seq<T> :: perm(p, m) && perm(m, q)) | |
} | |
lemma refl<T(!new)>(p: seq<T>) | |
ensures perm(p, p) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
predicate sorted (s: seq<int>) | |
{ | |
if |s| <= 1 then true else s[0] <= s[1] && sorted(s[1..]) | |
} | |
lemma {:induction m, n} sorted_elem_lemma(s: seq<int>, m: int, n: int) | |
decreases n - m | |
requires sorted(s) | |
requires 0 <= m <= n < |s| | |
ensures s[m] <= s[n] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang rosette | |
(require rosette/lib/angelic) | |
(define profession (list 'baker 'carpenter 'driver 'plumber)) | |
(define baker (apply choose* profession)) | |
(define carpenter (apply choose* profession)) | |
(define driver (apply choose* profession)) | |
(define plumber (apply choose* profession)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemma pigeonhole(m : int, n: int, f : int -> int) | |
requires 0 <= m < n | |
requires forall i :: 0 <= i < n ==> 0 <= f(i) < m | |
ensures exists j, k :: (0 <= j < k < n) && f(j) == f(k) | |
{ | |
if m <= 0 { | |
assert 0 <= f(0) < 0; | |
} | |
else { | |
var i : int := 0; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemma contains_implies_index (k : nat, perm : seq<nat>) | |
requires k in perm | |
ensures exists m :: 0 <= m < |perm| && perm[m] == k | |
{ | |
} | |
method next (perm: array<nat>) returns (res: bool) | |
modifies perm | |
requires forall k :: 1 <= k <= perm.Length ==> k in perm[..] | |
ensures !res ==> forall k :: 0 <= k < perm.Length ==> perm[k] == old(perm[k]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
include "./next_permutations_rank.dfy" | |
method copy (src: array<nat>, dest: array<nat>) | |
modifies dest | |
requires src.Length == dest.Length | |
ensures forall i :: 0 <= i < src.Length ==> dest[i] == src[i] | |
{ | |
var i := 0; | |
while i < src.Length | |
decreases src.Length - i |
NewerOlder