This file contains the unprocessed output of HOL4 on the two-way-sort example. A cleaned-up version with comments can be found here. It can be reproduced by running holfoot-full -f twowaysort.hol.
val SORTED_EL_DEF =
|- SORTED R L ⇔
(L = []) ∨ ∀n. n < LENGTH L − 1 ⇒ R (EL n L) (EL (SUC n) L):
thm
val dir = "": string
val file = "twowaysort.dsf": string
Contents of file "twowaysort.dsf":
--------------------------------------------
/* swap gets 3 call by value arguments: "a", "i", and "j".
The precondition states that there is an array in memory starting
at location "a", with size of constant "m". Moreover, the content
"data" of the array is specified explicitly.
The indices "i" and "j" are smaller than "m" and therefore the array accesses are
within the bound. */
swap (a,i,j) [data_array(a,#m,data) * i < #m * j < #m]{
local ti, tj;
/* Holfoot supports only very simple operations. There is no special
expressions or commands for arrays. Arrays are accessed using explicit
pointer arithmetic. For example, "(a+i) -> dta" means adding "i" to
the value of "a" and looking up the value stored in memory at this position
indexed by the tag "dta". More traditionally, it is written as "a[i]".
Moreover, memory lookups can not be used in expressions directly. They have
to be stored in a local variable first. Therefore, the code becomes: */
ti = (a + i) -> dta; /* ti <- a[i] */
tj = (a + j) -> dta; /* tj <- a[j] */
(a + j) -> dta = ti; /* a[j] <- ti */
(a + i) -> dta = tj; /* a[i] <- tj */
/* The post-condition states that there is still an array of the original size
at location m. However, the data content changed. It now contains the
original list with the elements at positions "i" and "j" swapped. The
quotation mark denote a HOL4-term. SWAP_ELEMENTS is a HOL4 function. */
} [data_array(a,#m,``SWAP_ELEMENTS j i data``)]
/* Holfoot does not support typing. All values are natural numbers. Therefore,
Boolean values are mapped to numbers (True => 1, False => 0).
The function "two_way_sort" gets two call-by-value arguments "a" and "m".
"a" is the location of an array containing some data "data". Because the
size is not stored in the array directly, the argument "m" is used to
pass the size of the array. The condition "m > 0" therefore demands that the
array is not empty. Moreover the pure condition
``EVERY IS_BOOL_TO_NUM data`` demands that only Boolean values
(i.e. only 0 and 1) are stored in the array. */
two_way_sort (a, m) [data_array (a, m, data) * m > 0 *
``EVERY IS_BOOL_TO_NUM data``] {
local i, j, temp;
i = 0;
j = m - 1;
while (i <= j)
/* The loop invariant says that there is always an
array of the right size at "a". This array contains some
existentially quantified data "_rdata". (Following Smallfoot,
the underscore is used to denote existential quantification).
Moreover, the upper index "j" is always smaller than
the size of the array. There is a pure side-condition as well.
It demands that "_rdata" is a permutation of "data" and that
"data" contains only Boolean values. Moreover all
array entries below "i" are 0, all above "j" are 1.
Notice that the termination of the loop is not proven. */
[data_array (a, m, _rdata) * j < m *
``(PERM data _rdata) /\
EVERY IS_BOOL_TO_NUM data /\
(!n. n < i ==> (EL n _rdata = 0)) /\
(!n. (j < n /\ n < m) ==> (EL n _rdata = 1))``] {
temp = (a + i) -> dta;
if (temp == 0) {
i = i+1;
} else {
temp = (a + j) -> dta;
if (temp == 1) {
j = j-1;
} else {
swap(a, i, j);
i = i+1;
j = j-1;
}
}
}
/* The post-condition guarantees that there is still the array
with size "m" at "a". However, it now contains some existentially
quantified data "_rdata" such that "_rdata" is a permutation of
the original data "data" and it is sorted according to the "<=" relation.
Holfoot uses fault avoiding semantics. Therefore, it is implicitly
guaranteed that all memory accesses were within the boundaries of the array.
Moreover it is guaranteed that there is no memory leak, i.e. that no junk
is left on the heap. */
} [data_array (a, m, _rdata) *
``(SORTED $<= _rdata) /\ (PERM data _rdata)``]
--------------------------------------------
val swap_TAC = fn: tactic
parsing ... 0.051 s - OK
HOLFOOT_SPECIFICATION (
swap(; a_const, i_const, j_const)
[w/r: ; | data_array(#a_const, #m, dta:data) ★ (#i_const < #m ) ★
(#j_const < #m )] {
local (a = a_const), (i = i_const), (j = j_const), ti, tj;
ti = (a + i)→dta;
tj = (a + j)→dta;
(a + j)→dta = ti;
(a + i)→dta = tj;
} [w/r: ; |
data_array(#a_const, #m,
dta:SWAP_ELEMENTS j_const i_const data)]
two_way_sort(; a_const, m_const)
[w/r: ; | data_array(#a_const, #m_const, dta:data) ★
(#m_const > 0) ★ pure(EVERY IS_BOOL_TO_NUM data)] {
local (a = a_const), (m = m_const), i, j, temp;
i = 0;
j = (m − 1);
/* Loop Invariant:
[w/r: i, j, temp; a, m | data_array(a, m, dta:_rdata) ★
(j < m) ★
pure(PERM !data _rdata ∧ EVERY IS_BOOL_TO_NUM !data ∧
(∀n. n < i ⇒ (EL n _rdata = 0)) ∧
∀n. j < n ∧ n < m ⇒ (EL n _rdata = 1))] */
while (i ≤ j) {
temp = (a + i)→dta;
if (temp = 0) {
i = (i + 1)
} else {
temp = (a + j)→dta;
if (temp = 1) {
j = (j − 1)
} else {
swap(; a, i, j); i = (i + 1); j = (j − 1);
};
};
};
} [w/r: ; | data_array(#a_const, #m_const, dta:_rdata) ★
pure(SORTED $<= _rdata ∧ PERM data _rdata)]
)
preprocessing ... 0.068 s - OK
verifying specification ...
* swap ... 0.301 s - OK
* two_way_sort ... 2.469 s - OK
done
time needed: 3.513 s
val final_thm =
|- HOLFOOT_SPECIFICATION (
swap(; a_const, i_const, j_const)
[w/r: ; | data_array(#a_const, #m, dta:data) ★
(#i_const < #m ) ★ (#j_const < #m )] {
local (a = a_const), (i = i_const), (j = j_const), ti, tj;
ti = (a + i)→dta;
tj = (a + j)→dta;
(a + j)→dta = ti;
(a + i)→dta = tj;
} [w/r: ; |
data_array(#a_const, #m,
dta:SWAP_ELEMENTS j_const i_const data)]
two_way_sort(; a_const, m_const)
[w/r: ; | data_array(#a_const, #m_const, dta:data) ★
(#m_const > 0) ★ pure(EVERY IS_BOOL_TO_NUM data)] {
local (a = a_const), (m = m_const), i, j, temp;
i = 0;
j = (m − 1);
/* Loop Invariant:
[w/r: i, j, temp; a, m | data_array(a, m, dta:_rdata) ★
(j < m) ★
pure(PERM !data _rdata ∧ EVERY IS_BOOL_TO_NUM !data ∧
(∀n. n < i ⇒ (EL n _rdata = 0)) ∧
∀n. j < n ∧ n < m ⇒ (EL n _rdata = 1))] */
while (i ≤ j) {
temp = (a + i)→dta;
if (temp = 0) {
i = (i + 1)
} else {
temp = (a + j)→dta;
if (temp = 1) {
j = (j − 1)
} else {
swap(; a, i, j); i = (i + 1); j = (j − 1);
};
};
};
} [w/r: ; | data_array(#a_const, #m_const, dta:_rdata) ★
pure(SORTED $<= _rdata ∧ PERM data _rdata)]
):
thm
val two_way_sort_TAC = fn: tactic