10.13 Input/output handling10.13 Input/output handling
10 C++ translator 10 C++ translator
10.14 An example

10.14 An example

This section explains how to translate and test the following specification of quicksort.

The parameter for QUICKSORT is the scheme QSP:

                                     
 scheme QSP =
 class
 type Elem
 
 value
 ≤ : Elem × Elem → Bool
 end

The parameterised QUICKSORT scheme is

                                     
 QSP
 
 scheme QUICKSORT(X : QSP) =
 with X in class
 value
 sort : Elem* → Elem*
 sort(l) ≡
 case l of
 〈〉 → 〈〉,
 〈h〉 ^ t →
 let (t1, t2) = split(h, t, 〈〉, 〈〉) in
 sort(t1) ^ 〈h〉 ^ sort(t2)
 end
 end,
 
 split :
 Elem × Elem* × Elem* × Elem* → Elem* × Elem*
 split(x, t, t1, t2) ≡
 case t of
 〈〉 → (t1, t2),
 〈h〉 ^ t3 →
 if h ≤ x then split(x, t3, 〈h〉 ^ t1, t2)
 else split(x, t3, t1, 〈h〉 ^ t2)
 end
 end
 end

To specify quicksort for integers we can create an object I for the actual parameter:

                                     
 object I : class type Elem = Int end

Quicksort is then scheme QI, which includes some test cases:

                                     
 QUICKSORT, I
 
 scheme QI =
 class
 object
 Q : QUICKSORT(I)
 test_case
 [t1]
 Q.sort(〈〉),
 [t2]
 Q.sort(〈12, 45, 2, 4, 2, 8, -1, 0〉)
 end

When this is compiled and the result executed, the output is as follows: 

[t1] <..>
[t2] <.-1,0,2,2,4,8,12,45.>

Checking the results for many such tests would be tedious. A better way is to have a more abstract specification of QUICKSORT like QSPEC:

                                     
 QSP
 
 scheme QSPEC(X : QSP) =
 with X in class
 value
 /* commented out for translation
 sort : Elem* → Elem*
 sort(l) as l′ post is_permutation(l, l′) /\ sorted(l′), */
 
 is_permutation : Elem* × Elem* → Bool
 is_permutation(l1, l2) ≡
 (∀ e : Elem •
  e ∈ elems l1 ∪ elems l2 ⇒
  count(l1, e) = count(l2, e)),
 
 count : Elem* × Elem → Nat
 count(l, e) ≡
 card {i | i : Int • i ∈ inds l /\ l(i) = e},
 
 sorted : Elem* → Bool
 sorted(l) ≡
 let s = inds l in
  (∀ i : Int • i ∈ s ⇒
  (∀ j : Int • j ∈ s ⇒
  j > i ⇒ l(i) ≤ l(j)))
 end
 end

Then we can instantiate both QUICKSORT and its more abstract specification and use the latter to check the former:

                                     
 QSPEC, QUICKSORT, I
 
 scheme QSI =
 class
 object
 A : QSPEC(I),
 B : QUICKSORT(I)
 
 value
 check : Int* → Bool
 check(l) ≡
 let l1 = B.sort(l) in
 A.is_permutation(l, l1) /\ A.sorted(l1)
 end
 
 test_case
 [t1] check(〈〉),
 [t2] check(〈1〉),
 [t3] check(〈1, 4, 3, 2, 7, 4, 6, 3, 8, 100, -2, -5, 8, 200〉)
 end

Translating, compiling, and running QSI produces the output 

[t1] true
[t2] true
[t3] true

This allows us to have many test cases (perhaps by random number generation) without the tedium of generating the expected results.

Chris George, April 17, 2008

10.14 An example
10.13 Input/output handling10.13 Input/output handling
10 C++ translator 10 C++ translator