Download code

Jump to: navigation, search

Back to Insertion_sort_(ACL2)

Download for Windows: single file, zip

Download for UNIX: single file, zip, tar.gz, tar.bz2

insertion-sort.lisp

 1 ; The authors of this work have released all rights to it and placed it
 2 ; in the public domain under the Creative Commons CC0 1.0 waiver
 3 ; (http://creativecommons.org/publicdomain/zero/1.0/).
 4 ; 
 5 ; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 6 ; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 7 ; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
 8 ; IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
 9 ; CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
10 ; TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
11 ; SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
12 ; 
13 ; Retrieved from: http://en.literateprograms.org/Insertion_sort_(ACL2)?oldid=11632
14 
15 (in-package "ACL2")
16 
17 (defun insert-sorted (a lst)
18   (if (or (endp lst)
19           (<= a (car lst)))
20       (cons a lst)
21     (cons (car lst) (insert-sorted a (cdr lst)))))
22 (defun insertion-sort (lst)
23   (if (endp lst)
24       lst
25     (insert-sorted (car lst) (insertion-sort (cdr lst)))))
26 
27 (defun is-ordered (lst)
28   (or (endp lst)
29       (endp (cdr lst))
30       (and (<= (car lst) (car (cdr lst)))
31            (is-ordered (cdr lst)))))
32 (defun delete-element (a lst)
33   (if (endp lst)
34       lst
35     (if (equal a (car lst))
36         (cdr lst)
37       (cons (car lst) (delete-element a (cdr lst))))))
38 (defun is-permutation (left right)
39   (or (and (endp left) (endp right))
40       (and (not (endp left))
41            (member (car left) right)
42            (is-permutation (cdr left) (delete-element (car left) right)))))
43 
44 
45 (defthm insert-sorted-has-input-as-member
46   (member a (insert-sorted a x)))
47 
48 (defthm insert-sorted-preserves-ordered
49   (implies (is-ordered x)
50            (is-ordered (insert-sorted a x))))
51 
52 (defthm delete-element-undoes-insert-sorted
53   (equal (delete-element a (insert-sorted a x))
54          x))
55 
56 (defthm insertion-sort-correct
57   (and (is-ordered (insertion-sort x))
58        (is-permutation x (insertion-sort x))))
59 
60 


hijacker
hijacker
hijacker
hijacker