globalvar arr=Array(3){arr.set(0,3)>>arr.set(1,2)>>arr.set(2,1)}

The above defines a global variable arr of type array, which has [3,2,1] as its initial value.

• def quicksort(a) =
•        def swap(x, y) = a.get(x) >z> a.set(x,a.get(y)) >> a.set(y,z)
• def part(p, s, t) =
•       def lr(i) = if i < t && a.get(i) <= p then lr(i+1) else i
•       def rl(i) = if a.get(i) > p then rl(i-1) else i
• (lr(s), rl(t)) >(s', t')>
• ( if (s' + 1 < t') >> swap(s', t') >> part(p, s'+1, t'-1)
• | if (s' + 1 = t') >> swap(s', t') >> s'
• | if (s' + 1 > t') >> t'
• ) def sort(s, t) =
• if s >= t then signal
• else part(a.get(s), s+1, t) >m>
• swap(m, s) >>
• (sort(s, m-1), sort(m+1, t)) >>
• signal
• sort(0, a.length()-1)

The above defines the quicksoft function. Its details can be found at [AQDKJM09].

quicksort(arr)

The above input the global variable arr for quicksorting.

#define sorted (arr.get(0)<arr.get(1) && arr.get(1)<arr.get(2))

The above defines a condition named as sorted which represents the situation where the number in the array is sorted in ascending order.

#assert System |= (<>sorted) && (sorted->[]sorted);

The assertion above specifies that eventually the array will be sorted, and once the array is sorted it will remain sorted.