@@ -70,7 +70,7 @@ lang: zh-tw
7070
7171### 霍爾式屬性 {#hoare-style-properties}
7272
73- [ 霍爾邏輯] ( https://en.wikipedia.org/wiki/Hoare_logic ) 提供了一套形式化規則，用於推理包括智慧型合約等程式的正確性。 霍爾式屬性使用霍爾三元組 ` {P}c{Q} ` 表示，其中 ` c ` 是一個程式， ` P ` 和 ` Q ` 為 ` c ` （即程式）的狀態述詞，正式描述分別為_前置條件_和_後置條件 _ 。
73+ [ 霍爾邏輯] ( https://en.wikipedia.org/wiki/Hoare_logic ) 提供了一套形式化規則，用於推理包括智慧型合約等程式的正確性。 A Hoare-style property is represented by a Hoare triple \{ _ P _ } _ c _ \{ _ Q _ }, where _ c _ is a program and _ P _ and _ Q _ are predicates on the state of the _ c _ (i.e., the program), formally described as _ preconditions _ and _ postconditions _ , respectively.
7474
7575前置條件是描述正確執行函式所需條件的述詞；叫用合約的使用者必須滿足該要求。 後置條件是描述函式正確執行時所建立之條件的述詞；使用者在叫用函式後可以預計該條件為 true。 在霍爾邏輯中，_ 不變量_是指透過執行函式保留的述詞（即，它不會改變）。
7676
@@ -212,16 +212,16 @@ function safe_add(uint x, uint y) returns(uint z){
212212
213213### 用於建立形式化規範的規範語言 {#specification-languages}
214214
215- ** Act** - _ * Act 允許指定存儲更新、前置/後置條件以及合約不變量。\{ 0}/0> 其工具套件還具有證明後端，可透過 Coq、SMT 求解器或 hevm 來證明許多屬性。**
215+ ** Act** - _ Act 允許指定存儲更新、前置/後置條件以及合約不變量。 其工具套件還具有證明後端，可透過 Coq、SMT 求解器或 hevm 來證明許多屬性。_
216216
217217- [ GitHub] ( https://github.com/ethereum/act )
218218- [ 文檔] ( https://ethereum.github.io/act/ )
219219
220- ** Scribble** - _ * Scribble 將以 Scribble 規範語言編寫的程式碼注解轉換爲用於檢查規範的具體斷言。**
220+ ** Scribble** - _ Scribble 將以 Scribble 規範語言編寫的程式碼注解轉換爲用於檢查規範的具體斷言。_
221221
222222- [ 文件] ( https://docs.scribble.codes/ )
223223
224- ** Dafny** — _ * Dafny 是一種驗證就緒的程式設計語言，仰賴高階註釋來推理和證明程式碼的正確性。**
224+ ** Dafny** — _ Dafny 是一種驗證就緒的程式設計語言，仰賴高階註釋來推理和證明程式碼的正確性。_
225225
226226- [ GitHub] ( https://github.com/dafny-lang/dafny )
227227
@@ -232,15 +232,15 @@ function safe_add(uint x, uint y) returns(uint z){
232232- [ 網站] ( https://www.certora.com/ )
233233- [ 文檔] ( https://docs.certora.com/en/latest/index.html )
234234
235- ** Solidity SMTChecker** - _ * Solidity 的 SMTChecker 是一個基於 SMT（可滿足性模數理論）和 Horn 求解的内置模型檢查器。 它在編譯期間確認合約的源程式碼是否符合規範，並以靜態方式檢查安全屬性的違反情況。**
235+ ** Solidity SMTChecker** - _ Solidity 的 SMTChecker 是一個基於 SMT（可滿足性模數理論）和 Horn 求解的内置模型檢查器。 它在編譯期間確認合約的源程式碼是否符合規範，並以靜態方式檢查安全屬性的違反情況。_
236236
237237- [ GitHub] ( https://github.com/ethereum/solidity )
238238
239- ** solc-verify** - _ * solc -verify 是 Solidity 編譯器的一個延伸版本，可以使用注解和模組化程式驗證在 Solidity 程式碼上執行自動形式化驗證。**
239+ ** solc-verify** - _ solc -verify 是 Solidity 編譯器的一個延伸版本，可以使用注解和模組化程式驗證在 Solidity 程式碼上執行自動形式化驗證。_
240240
241241- [ GitHub] ( https://github.com/SRI-CSL/solidity )
242242
243- ** KEVM** - _ * KEVM 是用 K 框架編寫的以太坊虛擬機 (EVM) 的形式化語義。 KEVM 是可執行的，並且可以用可達性邏輯來證明某些與屬性相關的斷言。**
243+ ** KEVM** - _ KEVM 是用 K 框架編寫的以太坊虛擬機 (EVM) 的形式化語義。 KEVM 是可執行的，並且可以用可達性邏輯來證明某些與屬性相關的斷言。_
244244
245245- [ GitHub] ( https://github.com/runtimeverification/evm-semantics )
246246- [ 文檔] ( https://jellopaper.org/ )
@@ -259,16 +259,16 @@ function safe_add(uint x, uint y) returns(uint z){
259259
260260### 用於偵測智慧型合約中易受攻擊模式的基於符號執行的工具 {#symbolic-execution-tools}
261261
262- ** Manticore** – _ * 一種基於符號執行的以太坊虛擬機位元組碼分析工具 * 。 *
262+ ** Manticore** – _ 一種基於符號執行的以太坊虛擬機位元組碼分析工具。 _
263263
264264- [ GitHub] ( https://github.com/trailofbits/manticore )
265265- [ 文檔] ( https://github.com/trailofbits/manticore/wiki )
266266
267- ** hevm** - _ * hevm 是用於以太坊虛擬機位元組碼的符號執行引擎和等價性檢查器。**
267+ ** hevm** - _ hevm 是用於以太坊虛擬機位元組碼的符號執行引擎和等價性檢查器。_
268268
269269- [ GitHub] ( https://github.com/dapphub/dapptools/tree/master/src/hevm )
270270
271- ** Mythril** - _ 用於檢測以太坊智慧型合約漏洞的符號執行工具 _
271+ ** Mythril** - _ 用於檢測以太坊智慧型合約漏洞的符號執行工具。 _
272272
273273- [ GitHub] ( https://github.com/ConsenSys/mythril-classic )
274274- [ 文檔] ( https://mythril-classic.readthedocs.io/en/develop/ )
0 commit comments