В заключение этой темы посмотрим, как проводилось тестирование работы с перегруженными методами:
/// <summary>
/// Тестирование перегруженных методов А()
/// </summary>
public void TestLoadMethods()
{
long u=0; double v =0;
A(out u, 7); A(out v, 7.5);
Console.WriteLine ("u= {0}, v= {1}", u,v);
A(out v,7);
Console.WriteLine("v= {0}",v);
A(out u, 7,11,13);
A(out v, 7.5, Math.Sin(11.5)+Math.Cos(13.5), 15.5);
Console.WriteLine ("u= {0}, v= {1}", u,v);
}//TestLoadMethods
На рис. 9.3 показаны результаты этого тестирования.
Рис. 9.3. Тестирование перегрузки методов
10. Корректность методов
Корректность метода. Спецификации. Триады Хоара. Предусловие метода. Постусловие метода. Корректность метода по отношению к предусловию и постусловию. Частичная корректность. Завершаемость. Полная корректность. Инвариант цикла. Вариант цикла. Подходящий инвариант. Корректность циклов. Рекурсия. Прямая и косвенная рекурсия. Стратегия "разделяй и властвуй". Сложность рекурсивных алгоритмов. Задача "Ханойские башни". Быстрая сортировка Хоара.
Написать метод, задающий ту или иную функциональность, нетрудно. Это может сделать каждый. Значительно сложнее написать метод, корректно решающий поставленную задачу. Корректность метода — это не внутреннее понятие, подлежащее определению в терминах самого метода. Корректность определяется по отношению к внешним спецификациям метода. Если нет спецификаций, то говорить о корректности "некорректно".
Спецификации можно задавать по-разному. Мы определим их здесь через понятия предусловий и постусловий метода, используя символику триад Хоара, введенных Чарльзом Энтони Хоаром — выдающимся программистом и ученым, одну из знаменитых программ которого приведем чуть позже в этой лекции.
Пусть P(x,z) — программа P с входными аргументами х и выходными z. Пусть Q(y) — некоторое логическое условие (предикат) над переменными программы у. Язык для записи предикатов Q(y) формализовать не будем. Отметим только, что он может быть шире языка, на котором записываются условия в программах, и включать, например, кванторы. Предусловием программы P(x,z) будем называть предикат Рrе(х), заданный на входах программы. Постусловием программы P(x,z) будем называть предикат Post(x,z), связывающий входы и выходы программы. Для простоты будем полагать, что программа P не изменяет своих входов х в процессе своей работы. Теперь несколько определений:
Определение 1 (частичной корректности): Программа P(x,z) корректна (частично, или условно) по отношению к предусловию Рrе(х) и постусловию Post(x,z), если из истинности предиката Рrе(х) следует, что для программы p(x,z)7 запущенной на входе х, гарантируется выполнение предиката Post(x,z) при условии завершения программы.
Условие частичной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:
[Pre(x)] P(x,z) [Post(х, z)]
Определение 2 (полной корректности): Программа P(x,z) корректна (полностью, или тотально) по отношению к предусловию Рrе(х) и постусловию Post(x,z), если из истинности предиката Рrе(х) следует, что для программы P(x,z), запущенной на входе х, гарантируется ее завершение и выполнение предиката Post(x,z).
Условие полной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:
{Pre(x) } Р (х, z) {Post(x,z) }
Доказательство полной корректности обычно состоит из двух независимых этапов — доказательства частичной корректности и доказательства завершаемости программы. Заметьте, полностью корректная программа, которая запущена на входе, не удовлетворяющем ее предусловию, вправе зацикливаться, а также возвращать любой результат. Любая программа корректна по отношению к предусловию, заданному тождественно ложным предикатом False. Любая завершающаяся программа корректна по отношению к постусловию, заданному тождественно истинным предикатом True.