函数/方法的后置条件

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 表示“所有”是标准的数学符号，如果您学过第一年的大学数学课程，您就会遇到它们。（可以说）有点不幸的是，人们使用的形式方法是种类或符号。它不必要地推迟/吓跑了绝大多数（通常）对数学感到不舒服的程序员。