Может ли SPARK доказать, что Quicksort действительно сортирует?

Question

Я не пользуюсь СПАРК. Я просто пытаюсь понять возможности языка.

Может ли SPARK доказать, например, что Quicksort действительно сортирует переданный ему массив?

Answer 1

Да, может, хотя я не особенно хорош в тестировании SPARK (пока). Вот как работает быстрая сортировка:

1. Отметим, что идея быстрой сортировки заключается в разделении.
2. Выбирается «точка поворота», которая используется для разделения коллекции на три группы: «равно», «меньше» и «больше». (Этот порядок влияет на процедуру, описанную ниже; я использую его, потому что он отличается от версии с порядком, чтобы проиллюстрировать, что в первую очередь речь идет о группировке, а не о порядке.)
3. Если коллекция есть или по длине, то вы сортируете; если тогда проверьте и, возможно, исправьте порядок, и они будут отсортированы; в противном случае продолжайте.
4. Переместите шарнир в первое положение.
5. Сканирование от второй позиции до последней позиции, в зависимости от рассматриваемого значения:
   1. - Поменять местами с первым элементом в разделе.
   2. - Нулевой режим.
   3. - Обмен с первым элементом, обмен с первым элементом.
6. Рекурсивно вызывать разделы &.
7. Если функция возвращает Less & Equal & Greater, если процедура перестроит in out вход в этот заказ.

Вот как бы вы поступили:

1. Доказать / отстаивать 0 а также 1 случаи как правда,
2. Докажите, что вы умеете обращаться с 2 Предметы,
3. Докажите, что для данной коллекции ввода и поворота существует набор из трех значений, которые представляют собой количество элементов меньше / равно / больше, чем точка поворота [это, вероятно, подпрограмма-призрак],
4. Докажите, что ++ равен длине вашей коллекции,
5. Докажите [в постусловии], что с учетом точки поворота и (L,E,G) кортеж, вывод соответствует L элементы меньше, чем точка поворота, за которой следует E элементы, которые равны, а затем G предметы, которые больше.

И это должно сработать. [IIUC]