Постусловие для функции / метода

Question

Кто-нибудь из вас документировал функцию или метод с предварительными и последующими условиями? (Я спрашиваю, потому что мой учитель говорит, что это официальный / правильный способ сделать это):

Легенда: (потому что я не мог набрать специальные символы) 3 - читать как «существует» и существовать
E - является членом (как в наборе)
A - для всех
-> - подразумевает

Предположим, что s непустая строка. Пусть B (s) будет множеством целых чисел, которые дают индексы позиций в строке s.
Вот начинается документация этой функции:

int FirstOccurence(String s, Char c)   
precondition: 
  (s.lenght() > 0) && 3 int i in B(s) [s.charAt(i) == c]    

это предварительное условие для постусловия;)

postcondition: 
  (FirstOccurence(s,c) E B(s)) && (s.charAt(FirstOccurence(s,c)) == c) && 
     A int i B(s)[(i < FirstOccurence(s,c)) --> !(s.charAt(i) == c) ]  

Кто-нибудь из вас когда-либо сталкивался с таким способом документирования функций / методов в реальном мире?

Answer 1

Да. Я сталкивался с этим, хотя это не обычная практика в промышленности.

В определенном контексте это определенно считается передовой практикой для формального указания предварительных условий , постусловий и инвариантов Например:

• при использовании формальных методов ; например для формального подтверждения правильности программ или
• при использовании языка программирования, такого как Eiffel, который поддерживает дизайн по контракту .

Если вам нужен пример того, как язык Eiffel поддерживает проектирование по контракту, посмотрите здесь .

---

Кстати, назад E для «существует» и вверх ногами A для «для всех» являются стандартными математическими обозначениями, и вы столкнулись бы с ними, если бы прошли 1-й курс университетской математики. Это (возможно) несколько неудачно, что формальные методы, которые используют люди, являются видом или обозначением. Это излишне отталкивает / отпугивает подавляющее большинство программистов, которым (в общем) не нравится математика.

Answer 2

Я также использовал его в университете и при документировании некоторых функций, где я нахожу это полезным.

В мире " real " это не так часто (ну, в общем, люди не так много документируют).

Я думаю, что любая документация хороша, и в тех случаях, когда не очень ясно, состояние параметров ввода / вывода до и после функции, предварительное условие и постусловие - это путь.

Кстати, в HTML вы можете использовать ∃ -> & Существовать; ∀ -> & forall; и некоторые другие символьные объекты: http://en.wikipedia.org/wiki/List_of_XML_and_HTML_character_entity_references

Answer 3

Cofoja (Контракты для Java) предоставляет Eiffel-подобные контракты с использованием аннотаций.

  @Requires({
    "h >= 0",
    "h <= 23"
  })
  @Ensures("getHour() == h")
  void setHour(int h);

Answer 4

Я написал до и после условия и инварианты классов формально.Проблема с ним возникает, когда нет критической массы, понимающей формальные обозначения.

Я должен признать, что мне требуется больше времени, чтобы понять A i in B(s): i < FirstOcc --> s[i] != c, чем просто: s has no occurence of c before firstOccurence(s,c).

Формализм полезен только тогда, когда

1. «интуитивно»понимание функции становится слишком сложным.Тогда вы можете использовать только формальные методы, чтобы доказать правильную реализацию или использование.
2. требуется автоматическая проверка

Взгляните, например, на sgi / stl документация.Они также используют полуформальные нотации, и слишком часто я вижу, как люди пытаются понять смысл задокументированных функций.

Answer 5

Spec # документы публикуют следующие условия:

static void Main(string![] args)
    requires args.Length > 0
{
    foreach(string arg in args)
    {
        Console.WriteLine(arg);
    }