math - 编程概念的数学符号

Question

有许多表示程序结构的方法（如 UML 类图等）。如果有一个以严格的数学方式描述程序的约定，我很感兴趣。我对为此目的使用数学符号特别感兴趣。

一个例子：类被表示为集合（字段、属性）和函数（对集合的元素进行操作）。父类的字段是子类的子集。函数用伪代码描述，必须看起来像这样和那样......

score 2 · Accepted Answer

我知道 Z Notation 已经在一定程度上用于软件的形式化验证，比如Tokeneer 项目。

score 2 · Accepted Answer

2

于 2009-10-27T19:33:04.210 回答

score 1 · Accepted Answer

1

于 2009-10-27T18:36:39.393 回答

score 1 · Accepted Answer

有很多方法，但我认为它们中的大多数不方便表达结构，因为结构通常无法用默认的数学概念表达。主要的例外当然是函数式编程语言。考虑折叠（catamorphisme）、群、代数等。

对于命令式编程，我知道 Z 的存在，它使用（纯和扩展的）lambda 演算集理论和（一阶）谓词逻辑。但是，我认为这不是很方便。使用数学来表达结构的唯一好处是你可以证明它的东西。但是，如果您想这样做，请查看 JML、Spec# 或 Eiffel。

score 1 · Accepted Answer

取决于您要完成的工作，但是使用特定语言走这条路可能会给您带来麻烦。

例如，请参阅C++ FAQ Lite 上的圆椭圆讨论。

score 1 · Accepted Answer

本书通过将程序与使它们能够工作的抽象数学理论联系起来，将演绎方法应用于编程。[...]

我相信Alexander Stepanov 和 Paul McJones 的Elements of Programming非常接近您正在寻找的内容。

概念

概念是对一种或多种类型的要求的描述，这些要求根据过程的存在和属性、类型属性和类型上定义的类型函数来说明。

score 1 · Accepted Answer

Z，已经提到过，几乎就是你所描述的。它有一些用于面向对象建模的变体，但我认为如果你想对类建模，你可以使用“标准 Z 的”模式走得很远。

还有Alloy，它更新并受 Z 启发。它的符号可能更接近于面向对象。它也是可分析的，即您可以检查您创建的模型是否满足某些条件，但它不能证明属性成立，只是尝试在有限范围内进行反驳。

设计的可靠软件一文很好地介绍了 Alloy 及其同类产品，以及可用的类似工具表。

score 1 · Accepted Answer

您正在寻找函数式编程。有几种函数式编程语言，它们都基于称为Lambda 演算的基本数学理论。用函数式编程语言（如 LISP）编写的程序是它们自身的数学表示。;-)

score 0 · Accepted Answer

有一种数学语言实际上描述了一个程序，或者更确切地说是它的操作。您采用初始状态，然后转换此状态，直到达到所需的目标状态。转换产生必须执行的程序代码。

基本思想是，对于每个函数（无论是将其放入类中还是放入旧式函数中），您都有一个前置条件和一个后置条件。例如，前提条件可以是您有一个包含>= 0元素的数组。后置条件是对于每个 i <= j，每个 element[i] 必须由 <= element[j]。

通常的描述是“函数对数组进行排序”。但是数学术语允许您将输入（必须匹配前置条件）转换为输出（必须匹配后置条件）。

使用起来有点笨拙，尤其是对于更复杂的程序，但其中一些示例令人印象深刻。通常，您会得到非常紧凑的代码，结果看起来很复杂，但在第一次尝试时就可以工作。

score 0 · Accepted Answer

我想推荐Algebra of Programming。这是一种程序的计算方法，使用关系代数和伽罗瓦连接。

如果您对这个主题有进一步的兴趣，您可以在这里找到一篇由 Shin-Cheng Mu 和 José Nuno Oliveira 撰写的精彩论文（幻灯片）。

使用关系代数和一阶逻辑，还与合金、函数式编程和契约式设计（很容易应用于面向对象的编程）有很好的协同作用。

10 回答 10