Example |
Example description |
Properties checked |
Command line |
bubbleSort |
A function that performs bubble sort on a list by swapping list elements. |
- Absence of null dereferences
- Output list is sorted in ascending order
- Output list is a permutation of the input list
|
tvla bubbleSort unsorted |
bubbleSort_bug |
A function that performs bubble sort on a list by swapping list elements. |
- Absence of null dereferences
- Output list is sorted in ascending order
- Output list is a permutation of the input list
|
tvla bubbleSort_bug unsorted |
insertSort |
A function that performs insertion sort on a list. |
- Absence of null dereferences
- Output list is sorted in ascending order
- Output list is a permutation of the input list
|
tvla insertSort unsorted |
insertSort_bug1 |
A function that performs insertion sort on a list. |
- Absence of null dereferences
- Output list is sorted in ascending order
- Output list is a permutation of the input list
|
tvla insertSort_bug1 unsorted |
insertSort_bug2 |
A function that performs insertion sort on a list. |
- Absence of null dereferences
- Output list is sorted in ascending order
- Output list is a permutation of the input list
|
tvla insertSort_bug2 unsorted |
merge |
A function that merges two sorted singly-linked lists into one sorted list. |
- Absence of null dereferences
- Merged list is sorted in ascending order
- Merged list contains all elements of the input lists
|
tvla merge merge |
reverse |
A function that reverses a sorted singly-linked list in-situ. |
- Absence of null dereferences
- Output list is sorted in descending order
|
tvla insertSort sorted |