Очень интересно и с юмором. Выводы:

Mechanical checks of simple properties enormously improve software quality:

Types ~ General but weak theorems (usually checked statically)

Contracts ~ General and strong theorems, checked dynamically for particular instances that occur during regular program operation

Unit tests ~ Specific and strong theorems, checked quasi-statically on particular “interesting instances”

Needed: Better ways of integrating these different sorts of checks

ЗЫ: Benjamin C. Pierce, кто не знает, автор Types and Programming Languages — одного из лучших учебников по теории типов.

Здравствуйте, deniok, Вы писали:

Ссылку-то и забыл

Здравствуйте, deniok, Вы писали:

Про линзы всё понятно... А где бананы и колючая проволока?

deniok,

D> Types ~ General but weak theorems (usually checked statically)

D> Contracts ~ General and strong theorems, checked dynamically for particular instances that occur during regular program operation

D> Unit tests ~ Specific and strong theorems, checked quasi-statically on particular “interesting instances”

Из презентации чувствуется, что Пирс полюбил контракты и что контракты ныне наше фсё.

Возьмём простейший стек, и зададимся вопросом: "какие контракты будут у ево методов?". Ответ: примерно такие

Автор: Lazy Cjow Rhrr
Дата: 12.07.06

Получается, что они конечно general, но на практике этот general будет весьма specific

Потом захочется хранить состояние в контрактах (ведь как-то надо выразить что до добавления элемента стек был размером n, а после добавления — (n+1)), потом осознаем что типы тоже неплохо бы там иметь. И циклы, чтобы буквы с клавиатуры не стёрлись раньше времени. И так далее и тому подобное. А в конце осознаем, что контракты — это частный случай метапрограмм, которые генерируют обычные ассерты

И юнит-тесты они тоже конечно specific, но в сочетании с регулярностью самой программы могут быть весьма general, например юнит тест для стека:

testSize()
{
    Stack s1 = new Stack(4);
    assertTrue(s1.size() == 0);
    s1.push("1");
    s1.push("2");
    s1.push("3");
    assertTrue(s1.size() == 3);
    assertExeption(s1.push("4"), Overflow.class); 
}

доказывает не только, что для стека размера 4 будут выполняться эти условия, а это будет доказывать справедливость и для стека произвольного размера n, потому что в соответствии с самим кодом фукций Stack, push и size у нас есть только 3 возможных состояния (пустой, непустой и полный) и мы их все протестили.

Так что, как мне кажется, и типы рано списывать со счетов, и юнит-тесты требуют более пристального теоретического исследования насчёт "free teorems" .

Здравствуйте, deniok, Вы писали:

D>Очень интересно и с юмором. Выводы:
D>

D> Types ~ General but weak theorems (usually checked statically)

D> Contracts ~ General and strong theorems, checked dynamically for particular instances that occur during regular program operation

D> Unit tests ~ Specific and strong theorems, checked quasi-statically on particular “interesting instances”
D>

D>Needed: Better ways of integrating these different sorts of checks
D>[/q]

Вообще мысль забавная: добавить к типам проверки значений и везде, где будет описан нужный тип, проверки вставятся автоматом. Этакие автоматизированные assert-ы. Но все-таки есть ощущение, что ничего нового в этой презентации пока нет, такие же инварианты/контракты, как в Eiffel, только с частичной статической типизацией.

Здравствуйте, vshabanov, Вы писали:

V>Вообще мысль забавная: добавить к типам проверки значений и везде, где будет описан нужный тип, проверки вставятся автоматом. Этакие автоматизированные assert-ы. Но все-таки есть ощущение, что ничего нового в этой презентации пока нет, такие же инварианты/контракты, как в Eiffel, только с частичной статической типизацией.

Ну там ссылка есть на работу Хинце с сотоварищами, вполне там контракты эфейлевские, даж помощней (хаскель всёж), плюс с выведением "виноватого".
Хотя так-то это всё то же, и для себе сильно большой выгоды в этом не вижу, разве что баги чуть быстрей находить можно, но есть же квикчек, да и собственный мозг, их никто не отменял вроде
Правда Пирс об обобщении этого всего вроде ратует, правда какое отношение линзы к этому имеют я не вкуриваю.

Курилка,

К>Хотя так-то это всё то же, и для себе сильно большой выгоды в этом не вижу, разве что баги чуть быстрей находить можно, но есть же квикчек, да и собственный мозг, их никто не отменял вроде

У quickcheck есть недостаток в том, что распределение тестовых данных нужно формировать самому. Вот если бы оно само делалось в зависимости от того, какие функции вызываются в тестах — мне кажется это было бы нереально круто

Есть работа, где авторы думают примерно в этом направлении ("Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution") но немного с другого боку. Нужно только объединить эти два подхода.

А собственный моск наверное лучше использовать на более творческие задачи, ежели написание юнит тестов

Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Курилка,

К>>Хотя так-то это всё то же, и для себе сильно большой выгоды в этом не вижу, разве что баги чуть быстрей находить можно, но есть же квикчек, да и собственный мозг, их никто не отменял вроде

LCR>У quickcheck есть недостаток в том, что распределение тестовых данных нужно формировать самому. Вот если бы оно само делалось в зависимости от того, какие функции вызываются в тестах — мне кажется это было бы нереально круто

У хинцевских контрактов тож самое, только они выдают ктож сбажил (в рамках разумного, конечно).
Т.е. контракт нарушается только в случае его проверки (т.е. конкретного теста)

LCR>Есть работа, где авторы думают примерно в этом направлении ("Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution") но немного с другого боку. Нужно только объединить эти два подхода.

LCR>А собственный моск наверное лучше использовать на более творческие задачи, ежели написание юнит тестов

Ага, я вот решил завязать с программированием

Курилка,

К>У хинцевских контрактов тож самое, только они выдают ктож сбажил (в рамках разумного, конечно).
К>Т.е. контракт нарушается только в случае его проверки (т.е. конкретного теста)

Не понял, что за зверь?

К>Ага, я вот решил завязать с программированием

Ого! Решил строить студентов? Али квадратики со стрелочками будешь рисовать?

Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Курилка,

К>>У хинцевских контрактов тож самое, только они выдают ктож сбажил (в рамках разумного, конечно).
К>>Т.е. контракт нарушается только в случае его проверки (т.е. конкретного теста)

LCR>Не понял, что за зверь?

Ну вот пишешь, пишешь...
(Эт я и про себя и про Пирса )
Ну глянь здесь

К>>Ага, я вот решил завязать с программированием

LCR>Ого! Решил строить студентов? Али квадратики со стрелочками будешь рисовать?

Да так, скорей админить, но может и студентами когда займусь...
Квадратики со стрелочками тоже уже несколько поднадоели (UML особливо)