Парочка мыслей.
Смотрю на Java Modelling Language, JML. В примере, данном в описании, код и спецификация разделены.
Например:
Как-то это нехорошо.
А на страничку JML я попал случайно, из списка инструментов статических проверок кода. Стало интересно, что же они там придумали. ;)
Теперь про тренировки.
Вчера я попытался жать на один раз. 120 кг едва-едва. Это я давно не тренировался. Но при этом 100-105 кг у меня рабочий вес в районе 6-10 повторений и, по идее, я должен был пожать где-то 125.
Налицо разница между теоретическим предсказанием и практическим результатом.
Например:
//@ requires amount > 0;
//@ ensures balance = \old(balance) + amount; -- спецификация
//@ assignable balance;
public void credit(int amount) { ... })Налицо дублирование кода.Как-то это нехорошо.
А на страничку JML я попал случайно, из списка инструментов статических проверок кода. Стало интересно, что же они там придумали. ;)
Теперь про тренировки.
Вчера я попытался жать на один раз. 120 кг едва-едва. Это я давно не тренировался. Но при этом 100-105 кг у меня рабочий вес в районе 6-10 повторений и, по идее, я должен был пожать где-то 125.
Налицо разница между теоретическим предсказанием и практическим результатом.
