Исправление SZT, (текущая версия) :
исчерпывающая формальная спецификация программы — это готовая программа.
Я могу вам дать формальную спецификацию сортировки, через которую можно доказать(которой должна соответствовать) корректность любой сортировки, и при этом готовой программой она являться не будет. А именно: я могу сказать что сортировка принимает на вход массив(или односвязный, двусвязный, xor-связный список и пр., от этого можно абстрагироваться. Далее будет просто «массив») фиксированного размера, состояший из чисел, и возвращает массив того же размера, из тех же самых чисел, имеющиеся в исходном входном массиве, притом каждое число должно встречаться во входном и в выходном массиве в том же количестве(т.е. если в сортируемом массиве было десять чисел 0 и пять 5, то в отсортированном тоже должно быть десять чисел 0 и пять 5) и каждый последующий элемент в этом сортированном массиве должен быть больше или равен предыдушему, в то время как к входным данным такого требования не предъявляется т.е. для любых возможных входных данных сортировка должна переупорядочить числа в порядке возрастания, и чтобы точно те же числа в том же количестве встречались как в сортированном, так и в несортированном массиве. И кроме того, добавим сюда условие завершаемости нашей сортировки. Все, вот вам полная спецификация, которой должна соответствовать ЛЮБАЯ корректная сортировка
Исправление SZT, :
исчерпывающая формальная спецификация программы — это готовая программа.
Я могу вам дать формальную спецификацию сортировки, через которую можно доказать корректность любой сортировки, и при этом готовой программой она являться не будет. А именно: я могу сказать что сортировка принимает на вход массив(или односвязный, двусвязный, xor-связный список и пр., от этого можно абстрагироваться. Далее будет просто «массив») фиксированного размера, состояший из чисел, и возвращает массив того же размера, из тех же самых чисел, имеющиеся в исходном входном массиве, притом каждое число должно встречаться во входном и в выходном массиве в том же количестве(т.е. если в сортируемом массиве было десять чисел 0 и пять 5, то в отсортированном тоже должно быть десять чисел 0 и пять 5) и каждый последующий элемент в этом сортированном массиве должен быть больше или равен предыдушему, в то время как к входным данным такого требования не предъявляется т.е. для любых возможных входных данных сортировка должна переупорядочить числа в порядке возрастания, и чтобы точно те же числа в том же количестве встречались как в сортированном, так и в несортированном массиве. И кроме того, добавим сюда условие завершаемости нашей сортировки. Все, вот вам полная спецификация, которой должна соответствовать ЛЮБАЯ корректная сортировка
Исходная версия SZT, :
исчерпывающая формальная спецификация программы — это готовая программа.
Я могу вам дать формальную спецификацию сортировки, через которую можно доказать корректность любой сортировки. А именно: я могу сказать что сортировка принимает на вход массив(или односвязный, двусвязный, xor-связный список и пр., от этого можно абстрагироваться. Далее будет просто «массив») фиксированного размера, состояший из чисел, и возвращает массив того же размера, из тех же самых чисел, имеющиеся в исходном входном массиве, притом каждое число должно встречаться во входном и в выходном массиве в том же количестве(т.е. если в сортируемом массиве было десять чисел 0 и пять 5, то в отсортированном тоже должно быть десять чисел 0 и пять 5) и каждый последующий элемент в этом сортированном массиве должен быть больше или равен предыдушему, в то время как к входным данным такого требования не предъявляется т.е. для любых возможных входных данных сортировка должна переупорядочить числа в порядке возрастания, и чтобы точно те же числа в том же количестве встречались как в сортированном, так и в несортированном массиве. И кроме того, добавим сюда условие завершаемости нашей сортировки. Все, вот вам полная спецификация, которой должна соответствовать ЛЮБАЯ корректная сортировка