Max(seq) == LET set == {seq[i]: i \in 1..Len(seq)} IN CHOOSE x \in set: \A y \in set: y <= x
AllInputs == PT!SeqOf(IntSet, MaxSeqLen)
(*—algorithm max variables seq \in AllInputs, i = 1, max; begin max := seq[1]; while i <= Len(seq) do if max < seq[i] then max := seq[i]; end if; i := i + 1; end while; assert max = Max(seq); end algorithm; *)
begin output := in_str; while Len(output) < in_n do output := <<in_c>> \o output; end while; assert output = Leftpad(in_c, in_n, in_str); end algorithm; *)
OrderedSeqOf(set, n) == { seq \in PT!SeqOf(set, n): \A x \in 2..Len(seq): seq[x] >= seq[x-1] } MaxInt == 4 Range(f) == {f[x]: x \in DOMAIN f} (*—algorithm definitely_binary_search variables i = 1, seq \in OrderedSeqOf(1..MaxInt, MaxInt), target \in 1..MaxInt, found_index = 0; begin Search: while i <= Len(seq) do if seq[i] = target then found_index := i; goto Result; else i := i + 1; end if; end while; Result: if target \in Range(seq) then assert seq[found_index] = target; else \* 0 is out of DOMAIN seq, so can represent ”not found“ assert found_index = 0; end if; end algorithm; *)
variables i = 1, seq \in OrderedSeqOf(1..MaxInt, MaxInt), target \in 1..MaxInt, found_index = 0, counter = 0; 🔆新增的次数计数器 Search: while i <= Len(seq) do counter := counter + 1; 🔆 if seq[i] = target then found_index := m; goto Result; end if; i := i + 1 end while; Result: ⚠️在这里增加检查 if Len(seq) > 0 then assert Pow2(counter-1) <= Len(seq); end if; if target \in PT!Range(seq) then assert seq[found_index] = target; else assert found_index = 0; end if;
(*--algorithm binary_search variables low = 1, seq \in OrderedSeqOf(1..MaxInt, MaxInt), high = Len(seq), target \in 1..MaxInt, found_index = 0, counter = 0; begin Search: while low <= high do counter := counter + 1; with m = (high + low) \div 2 do if seq[m] = target then found_index := m; goto Result; elsif seq[m] < target then low := m + 1; else high := m - 1; end if; end with; end while; Result: if Len(seq) > 0 then assert Pow2(counter-1) <= Len(seq); end if; if target \in Range(seq) then assert seq[found_index] = target; else assert found_index = 0; end if; end algorithm; *)
上面例子中有一个微妙的错误：low + high可能会超过机器上的整数的范围。下面检查了：
这样会失败。可以改成：
给一个专门用于检查溢出的不变量：
1 2 3
NoOverflows == \A x \in {m, lh, low, high}: x <= MaxInt
fair process incrementer \in 1..3 variable local = 0 begin Get: local := counter; Increment: counter := local + 1; end process;
end algorithm; *)
This, unsurprisingly, fails, as our processes can increment based off stale memory. If we merge the two labels into one label, this succeeds with 22 states.
