編程概念的數學表示法

Question

表示程序結構的許多方法（如UML類圖等）。如果有一個以嚴格的數學方式描述程序的慣例，我很感興趣。我特別感興趣的是爲此使用數學符號。

示例：類表示爲集（字段，屬性）和函數（對集合的元素進行操作）。父類'字段是子類的子集'。函數在僞代碼中描述，它必須看起來像這樣並且...

Answer 1

我知道Z Notation在軟件的正式驗證中已經有所應用，比如the Tokeneer project。

Z Notation

Z Reference Manual

Answer 2

是的，有，Floyd-Hoare Logic。

Answer 3

有很多方法，但我認爲他們中的大多數不方便表達結構，因爲結構通常在默認數學概念中不可表達。主要的例外當然是功能性編程語言。考慮摺疊（catamorphisme），組，代數等等。對於命令式編程，我知道Z的存在，它使用（純粹的和擴展的）lambda微積分集合論和（一階）謂詞邏輯。但是，我不認爲這很方便。使用數學表達結構的唯一好處是你可以證明它的一些事實。但如果你想這樣做，看看JML，Spec＃或Eiffel。

Answer 4

取決於你想要完成的任務，但是用特定語言走這條路可能會讓你陷入困境。

例如，請參閱C++ FAQ Lite上的circle-ellipse discussion。

Answer 5

本書適用演繹法 編程通過建立聯盟關係計劃 與抽象的數學理論 ，使他們的工作。 [...]

我相信亞歷山大Stepanov和保羅麥克瓊斯Elements of Programming，是非常接近你在找什麼。

Concepts

的一個概念是對一種或多種類型 要求在存在的條件和程序 特性陳述的描述，類型 屬性和類型的功能的類型定義 。

Answer 6

有一種數學語言實際上描述了一個程序，或者說它的操作。您採取初始狀態，然後轉換此狀態，直到達到所需的目標狀態。轉換產生必須執行的程序代碼。

查看Wikipedia article about Hoare logic。

其基本思想是對於每個功能（無論是將其放入班級還是放入舊式功能中），都有前置條件和後置條件。例如，前提條件可能是您有一個包含>= 0元素的數組。後置條件是每個元素[i]必須由< =元素[j]爲每個i < = j。

通常的描述是「函數對數組進行排序」。但是，數學術語允許您將輸入（必須匹配前提條件）轉換爲輸出（必須匹配後置條件）。

使用起來有點笨拙，特別是對於更復雜的程序，但其中一些例子非常令人印象深刻。通常情況下，你會得到非常緊湊的代碼，因爲結果看起來相當複雜，但是可以在第一時間嘗試。

Answer 7

http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/dp/0201558025

Answer 8

Z，這已經提到，幾乎是你描述。對於面向對象的建模，它有一些變體，但是我認爲如果你希望對類進行建模，你可以用「標準Z的」模式獲得相當的效果。

也有Alloy，這是更新和靈感來自Z.它的符號可能更接近於面向對象。這也是可以分析的，即你可以檢查你創建的模型是否滿足某些條件，但它不能證明屬性是否成立，只是試圖在有限範圍內進行反駁。

文章Dependable Software by Design是一個很好的介紹合金及其同類，以及一個可用的類似工具表。

Answer 9

您在找functional programming.有幾種函數式編程語言，它們都基於一個基本的數學理論，稱爲Lambda calculus。用諸如LISP之類的函數式編程語言編寫的程序是它們自己的數學表示。 ;-)

Answer 10

我想提議編程代數。這是一種計算方法，使用Relational Algebra和Galois Connections。

如果您對此主題有進一步的興趣，您可以找Shin-Cheng Mu和JoséNuno Oliveira（slides）的優秀論文here。

使用關係代數和一階邏輯，與Alloy，函數式編程和契約式設計（很容易應用於面向對象編程）也有很好的協同作用。