diff --git a/public/content/translations/de/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/de/developers/docs/smart-contracts/formal-verification/index.md index 6b01aff253a..c6fc119f41b 100644 --- a/public/content/translations/de/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/de/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Formale Spezifizierungen auf Low-Level-Ebene können in Form von entweder Eigens ### Hoare-Stil-Eigenschaften {#hoare-style-properties} -Die [Hoare-Logik](https://en.wikipedia.org/wiki/Hoare_logic) bietet eine Reihe von formalen Regeln für Schlussfolgerungen über die Korrektheit von Programmen, einschließlich der von Smart Contracts. Eine Eigenschaft im Hoare-Stil wird durch ein Hoare-Tripel \{_P_}_c_\{_Q_} dargestellt, wobei _c_ ein Programm ist und _P_ und _Q_ Prädikate über den Zustand von _c_ (d.h. das Programm) sind, die formal als _Präkonditionen_ bzw. _Postkonditionen_ beschrieben werden. +Die [Hoare-Logik](https://en.wikipedia.org/wiki/Hoare_logic) bietet eine Reihe von formalen Regeln für Schlussfolgerungen über die Korrektheit von Programmen, einschließlich der von Smart Contracts. Eine Eigenschaft im Hoare-Stil wird durch ein Hoare-Tripel `{P}c{Q}` dargestellt, wobei `c` ein Programm ist und `P` und `Q` Prädikate über den Zustand von `c` (d.h. das Programm) sind, die formal als _Präkonditionen_ bzw. _Postkonditionen_ beschrieben werden. Eine Präkondition ist ein Prädikat, das die für die korrekte Ausführung einer Funktion erforderlichen Bedingungen beschreibt; Benutzer, die den Vertrag aufrufen, müssen diese Bedingung erfüllen. Eine Nachbedingung ist ein Prädikat, das die Bedingung beschreibt, die eine Funktion bei korrekter Ausführung festlegt; die Benutzer können davon ausgehen, dass diese Bedingung nach dem Aufruf der Funktion als erfüllt gilt. Eine _Invariante_ in der Hoare-Logik ist ein Prädikat, das durch die Ausführung einer Funktion erhalten bleibt (d. h. sich nicht verändert). diff --git a/public/content/translations/el/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/el/developers/docs/smart-contracts/formal-verification/index.md index 41f0171855d..8e51d7f8193 100644 --- a/public/content/translations/el/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/el/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: el ### Ιδιότητες τύπου Hoare {#hoare-style-properties} -Η [λογική Hoare](https://en.wikipedia.org/wiki/Hoare_logic) παρέχει ένα σύνολο τυπικών κανόνων για τον συλλογισμό σχετικά με τη σωστή λειτουργία των προγραμμάτων, συμπεριλαμβανομένων των έξυπνων συμβολαίων. Μια ιδιότητα τύπου Hoare αντιπροσωπεύεται από ένα τριπλό Hoare \{_P_}_c_\{_Q_}, όπου το _c_ είναι ένα πρόγραμμα και τα _P_ και _Q_ είναι προτάσεις για την κατάσταση του _c_ (δηλαδή, του προγράμματος), που περιγράφονται επίσημα ως _προϋποθέσεις_ και _μετα-συνθήκες_, αντίστοιχα. +Η [λογική Hoare](https://en.wikipedia.org/wiki/Hoare_logic) παρέχει ένα σύνολο τυπικών κανόνων για τον συλλογισμό σχετικά με τη σωστή λειτουργία των προγραμμάτων, συμπεριλαμβανομένων των έξυπνων συμβολαίων. Μια ιδιότητα τύπου Hoare αντιπροσωπεύεται από ένα τριπλό Hoare `{P}c{Q}`, όπου το `c` είναι ένα πρόγραμμα και τα `P` και `Q` είναι προτάσεις για την κατάσταση του `c` (δηλαδή, του προγράμματος), που περιγράφονται επίσημα ως _προϋποθέσεις_ και _μετα-συνθήκες_, αντίστοιχα. Μια προϋπόθεση είναι μια πρόταση που περιγράφει τις συνθήκες που απαιτούνται για τη σωστή εκτέλεση μιας συνάρτησης. Οι χρήστες που καλούν το συμβόλαιο πρέπει να ικανοποιούν αυτήν την απαίτηση. Μια μετα-συνθήκη είναι μια πρόταση που περιγράφει την κατάσταση που καθορίζει μια συνάρτηση εάν εκτελεστεί σωστά. Οι χρήστες μπορούν να αναμένουν ότι αυτή η συνθήκη θα είναι αληθής μετά την κλήση της συνάρτησης. Ένα _αμετάβλητο στοιχείο_ στη λογική Hoare είναι μια πρόταση που διατηρείται με εκτέλεση συνάρτησης (δηλαδή, δεν αλλάζει). diff --git a/public/content/translations/es/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/es/developers/docs/smart-contracts/formal-verification/index.md index 821a3e47c07..f35d960f00f 100644 --- a/public/content/translations/es/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/es/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Las especificaciones formales de bajo nivel se pueden dar como propiedades de es ### Propiedades de estilo Hoare {#hoare-style-properties} -La [lógica de Hoare](https://en.wikipedia.org/wiki/Hoare_logic) proporciona un conjunto de reglas formales para razonar sobre la corrección de los programas, incluidos los contratos inteligentes. Una propiedad de estilo Hoare está representada por un triple Hoare \{_P_}_c_\{_Q_}, donde _c_ es un programa y _P_ y _Q_ son predicados sobre el estado del _c_ (es decir, el programa), descrito formalmente como _precondiciones_ y _poscondiciones_, respectivamente. +La [lógica de Hoare](https://en.wikipedia.org/wiki/Hoare_logic) proporciona un conjunto de reglas formales para razonar sobre la corrección de los programas, incluidos los contratos inteligentes. Una propiedad de estilo Hoare está representada por un triple Hoare `{P}c{Q}`, donde `c` es un programa y `P` y `Q` son predicados sobre el estado del `c` (es decir, el programa), descrito formalmente como _precondiciones_ y _poscondiciones_, respectivamente. Una precondición es un predicado que describe las condiciones requeridas para la correcta ejecución de una función; los usuarios que invocan o llaman al contrato deben cumplir con este requisito. Una poscondición es un predicado que describe la condición que una función establece si se ejecuta correctamente; los usuarios pueden esperar que esta condición sea verdadera después de invocar la función. Un _invariante_ en la lógica de Hoare es un predicado que se conserva mediante la ejecución de una función (es decir, no cambia). diff --git a/public/content/translations/fa/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/fa/developers/docs/smart-contracts/formal-verification/index.md index 8ee2682c367..51f20781d37 100644 --- a/public/content/translations/fa/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/fa/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: fa ### خواص سبک هوآر {#hoare-style-properties} -[منطق هوآر](https://en.wikipedia.org/wiki/Hoare_logic) مجموعه‌ای از قوانین رسمی را برای استدلال در مورد صحت برنامه‌ها، از جمله قراردادهای هوشمند، ارائه می‌کند. یک ویژگی به سبک هوآر با یک سه‌گانه هوآر \{_P_}_c_\{_Q_} نشان داده می‌شود، که در آن _c_ یک برنامه است و _P_ و _Q_ گزاره‌هایی در مورد حالت c (یعنی برنامه) هستند که به ترتیب به صورت _پیش شرط‌ها_ و _پس شرط‌ها_ توصیف می‌شوند. +[منطق هوآر](https://en.wikipedia.org/wiki/Hoare_logic) مجموعه‌ای از قوانین رسمی را برای استدلال در مورد صحت برنامه‌ها، از جمله قراردادهای هوشمند، ارائه می‌کند. یک ویژگی به سبک هوآر با یک سه‌گانه هوآر `{P}c{Q}` نشان داده می‌شود، که در آن `c` یک برنامه است و `P` و `Q` گزاره‌هایی در مورد حالت c (یعنی برنامه) هستند که به ترتیب به صورت _پیش شرط‌ها_ و _پس شرط‌ها_ توصیف می‌شوند. پیش شرط یک گزاره است که شرایط لازم برای اجرای صحیح یک تابع را توصیف می کند. کاربرانی که قرارداد را امضا می کنند باید این شرط را برآورده کنند. پیش شرط یک گزاره است که شرایط لازم برای اجرای صحیح یک تابع را توصیف می کند. کاربرانی که قرارداد را امضا کنند باید این شرط را تعیین کنند. یک _ثابت_ در منطق هوآر یک گزاره است که توسط اجرای یک تابع حفظ می‌شود (یعنی تغییر نمی‌کند). diff --git a/public/content/translations/fr/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/fr/developers/docs/smart-contracts/formal-verification/index.md index d7af618674d..7c43dec0543 100644 --- a/public/content/translations/fr/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/fr/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Les spécifications formelles de bas niveau peuvent être données sous forme de ### Propriétés de style Hoare {#hoare-style-properties} -[La logique Hoare](https://en.wikipedia.org/wiki/Hoare_logic) fournit un ensemble de règles formelles pour raisonner sur la correction des programmes, y compris les contrats intelligents. Une propriété de style Hoare est représentée par un triple Hoare \{_P_}_c_\{_Q_}, où _c_ est un programme et _P_ et _Q_ sont des prédicats sur l'état de _c_ (c'est-à-dire le programme), formellement décrits comme des _prérequis_ et des _conditions ulérieures_, respectivement. +[La logique Hoare](https://en.wikipedia.org/wiki/Hoare_logic) fournit un ensemble de règles formelles pour raisonner sur la correction des programmes, y compris les contrats intelligents. Une propriété de style Hoare est représentée par un triple Hoare `{P}c{Q}`, où `c` est un programme et `P` et `Q` sont des prédicats sur l'état de `c` (c'est-à-dire le programme), formellement décrits comme des _prérequis_ et des _conditions ulérieures_, respectivement. Un prérequis est un prédicat décrivant les conditions requises pour l'exécution correcte d'une fonction ; les utilisateurs qui font appel au contrat doivent satisfaire à cette exigence. Une condition ultérieure est un prédicat décrivant la condition qu'une fonction établit si elle est correctement exécutée ; les utilisateurs peuvent s'attendre à ce que cette condition soit vraie après avoir appelé la fonction. Un _invariant_ en logique Hoare est un prédicat qui est préservé par l'exécution d'une fonction (c'est-à-dire qu'il ne change pas). diff --git a/public/content/translations/hi/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/hi/developers/docs/smart-contracts/formal-verification/index.md index b05417d04c6..c4062fff654 100644 --- a/public/content/translations/hi/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/hi/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: hi ### होरे-शैली के गुण {#hoare-style-properties} -[होरे लॉजिक](https://en.wikipedia.org/wiki/Hoare_logic) स्मार्ट अनुबंधों सहित कार्यक्रमों की शुद्धता के बारे में तर्क के लिए औपचारिक नियमों का एक सेट प्रदान करता है। एक होरे-शैली की विशेषता को होरे ट्रिपल \{_P_}_c_\{_Q_} द्वारा दर्शाया जाता है, जहां _c_ एक प्रोग्राम है और _P_ और _Q_ _c_ (यानी, कार्यक्रम) की स्थिति पर विधेय हैं, औपचारिक रूप से क्रमशः _प्रीकंडीशंस_ और _पोस्टकंडीशन_ के रूप में वर्णित हैं। +[होरे लॉजिक](https://en.wikipedia.org/wiki/Hoare_logic) स्मार्ट अनुबंधों सहित कार्यक्रमों की शुद्धता के बारे में तर्क के लिए औपचारिक नियमों का एक सेट प्रदान करता है। एक होरे-शैली की विशेषता को होरे ट्रिपल `{P}c{Q}` द्वारा दर्शाया जाता है, जहां `c` एक प्रोग्राम है और `P` और `Q` `c` (यानी, कार्यक्रम) की स्थिति पर विधेय हैं, औपचारिक रूप से क्रमशः _प्रीकंडीशंस_ और _पोस्टकंडीशन_ के रूप में वर्णित हैं। एक पूर्व शर्त एक विधेय है जो किसी फ़ंक्शन के सही निष्पादन के लिए आवश्यक शर्तों का वर्णन करता है; अनुबंध में कॉल करने वाले उपयोगकर्ताओं को इस आवश्यकता को पूरा करना होगा। एक पोस्टकंडीशन एक विधेय है जो उस स्थिति का वर्णन करता है जिससे एक फ़ंक्शन लागू होता है अगर सही ढंग से लागू किया जाता है; उपयोगकर्ता फ़ंक्शन में कॉल करने के बाद इस स्थिति के सत्य होने की उम्मीद कर सकते हैं। होरे लॉजिक में एक _इनवेरिएंट_ एक विधेय है जिसे किसी फ़ंक्शन के निष्पादन द्वारा संरक्षित किया जाता है (यानी, यह नहीं बदलता है)। diff --git a/public/content/translations/hu/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/hu/developers/docs/smart-contracts/formal-verification/index.md index bd51daf500f..fe656d69d52 100644 --- a/public/content/translations/hu/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/hu/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Az alacsony szintű formális specifikációkat Hoare-stílusú tulajdonságokk ### Hoare-stílusú tulajdonságok {#hoare-style-properties} -A [Hoare-logika](https://en.wikipedia.org/wiki/Hoare_logic) egy sor formális szabályt biztosít a programok, köztük az okosszerződések helyességére vonatkozó érveléshez. Egy Hoare-stílusú tulajdonságot egy Hoare-hármas \{_P_}_c_\{_Q_} reprezentál, ahol _c_ egy program, _P_ és _Q_ állítások a _c_ státuszára (a programra) vonatkozóan, amelyeket formálisan _előfeltételekkel_ és _utófeltételekkel_ írunk le. +A [Hoare-logika](https://en.wikipedia.org/wiki/Hoare_logic) egy sor formális szabályt biztosít a programok, köztük az okosszerződések helyességére vonatkozó érveléshez. Egy Hoare-stílusú tulajdonságot egy Hoare-hármas `{P}c{Q}` reprezentál, ahol `c` egy program, `P` és `Q` állítások a `c` státuszára (a programra) vonatkozóan, amelyeket formálisan _előfeltételekkel_ és _utófeltételekkel_ írunk le. Az előfeltétel egy állítás, amely leírja a függvény helyes végrehajtásához szükséges feltételeket; a szerződést meghívó felhasználóknak meg kell felelniük ennek a követelménynek. Az utófeltétel egy állítás, amely azt a feltételt írja le, amelyet egy függvény helyesen végrehajtva állít fel; a felhasználók elvárhatják, hogy ez a feltétel igaz legyen a függvény meghívása után. A _konstans_ a Hoare-logikában olyan állítás, amely egy függvény végrehajtása során megmarad (nem változik). diff --git a/public/content/translations/it/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/it/developers/docs/smart-contracts/formal-verification/index.md index ff79bfacf8a..98898c96b87 100644 --- a/public/content/translations/it/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/it/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Le specifiche formali di basso livello possono essere date come proprietà in st ### Proprietà in stile Hoare {#hoare-style-properties} -La [logica di Hoare](https://en.wikipedia.org/wiki/Hoare_logic) fornisce una serie di regole formali per ragionare sulla correttezza dei programmi, contratti intelligenti inclusi. Una proprietà in stile Hoare è rappresentata da una tripletta di Hoare \{_P_}_c_\{_Q_}, dove _c_ è un programma e _P_ e _Q_ sono predicati sullo stato della _c_ (cioè, il programma), formalmente descritte rispettivamente come _precondizioni_ e _postcondizioni_. +La [logica di Hoare](https://en.wikipedia.org/wiki/Hoare_logic) fornisce una serie di regole formali per ragionare sulla correttezza dei programmi, contratti intelligenti inclusi. Una proprietà in stile Hoare è rappresentata da una tripletta di Hoare `{P}c{Q}`, dove `c` è un programma e `P` e `Q` sono predicati sullo stato della `c` (cioè, il programma), formalmente descritte rispettivamente come _precondizioni_ e _postcondizioni_. Una precondizione è un predicato che descrive le condizioni richieste per l'esecuzione corretta di una funzione; gli utenti che chiamano il contratto devono soddisfare tale requisito. Una postcondizione è un predicato che descrive la condizione che una funzione stabilisce se eseguita correttamente; gli utenti possono prevedere che questa condizione sia vera dopo aver chiamato la funzione. Un'_invariante_ nella logica di Hoare è un predicato che è preservato dall'esecuzione di una funzione (cioè, non cambia). diff --git a/public/content/translations/ja/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/ja/developers/docs/smart-contracts/formal-verification/index.md index 30b4b561048..c5e372848f2 100644 --- a/public/content/translations/ja/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/ja/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: ja ### ホーア型のプロパティ {#hoare-style-properties} -[ホーア論理](https://en.wikipedia.org/wiki/Hoare_logic)は、スマートコントラクトなどのプログラムの正当性を論証するための形式規則を提供します。 ホーア型のプロパティは、ホーアトリプルと呼ばれる\{_P_}_c_\{_Q_}という形の式で与えられます。_c_はプログラムで、_P_と_Q_はそれぞれ正式には_事前条件_、_事後条件_と呼ばれる、cの状態についての述語です。 +[ホーア論理](https://en.wikipedia.org/wiki/Hoare_logic)は、スマートコントラクトなどのプログラムの正当性を論証するための形式規則を提供します。 ホーア型のプロパティは、ホーアトリプルと呼ばれる`{P}c{Q}`という形の式で与えられます。`c`はプログラムで、`P`と`Q`はそれぞれ正式には_事前条件_、_事後条件_と呼ばれる、cの状態についての述語です。 事前条件は関数を正しく実行するために求められる条件を表しています。スマートコントラクトを呼び出す際には、この事前条件が満たされている必要があります。 事後条件は、関数が正しく実行された場合に成立する条件を表しています。関数呼び出しの後はこの事後条件が真となることが期待されます。 ホーア論理の_不変条件_は、関数の実行中は常に維持されます(すなわち、変化しません)。 diff --git a/public/content/translations/pt-br/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/pt-br/developers/docs/smart-contracts/formal-verification/index.md index 1fe8dbe872e..9ff72b630c0 100644 --- a/public/content/translations/pt-br/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/pt-br/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Especificações formais de baixo nível podem ser fornecidas como propriedades ### Propriedades do estilo Hoare {#hoare-style-properties} -[Hore Logic](https://en.wikipedia.org/wiki/Hoare_logic) fornece um conjunto de regras formais para raciocinar sobre a correção de programas, incluindo contratos inteligentes. Uma propriedade de estilo Hoare é representada por um triplo Hoare \{_P_}_c_\{_Q_}, onde _c_ é um programa e _P_ e _Q_ são predicados no estado do _c_ (ou seja, o programa), formalmente descritos como _precondições_ e _pós-condições_, respectivamente. +[Hore Logic](https://en.wikipedia.org/wiki/Hoare_logic) fornece um conjunto de regras formais para raciocinar sobre a correção de programas, incluindo contratos inteligentes. Uma propriedade de estilo Hoare é representada por um triplo Hoare `{P}c{Q}`, onde `c` é um programa e `P` e `Q` são predicados no estado do `c` (ou seja, o programa), formalmente descritos como _precondições_ e _pós-condições_, respectivamente. Uma precondição é um predicado que descreve as condições necessárias para a execução correta de uma função; os usuários que chamam um contrato devem satisfazer este requisito. Uma pós-condição é um predicado que descreve a condição que uma função estabelece se executada corretamente; os usuários podem esperar que essa condição seja verdadeira após chamar a função. Uma _invariável_ na lógica Hoare é um predicado que é preservado pela execução de uma função (ou seja, não muda). diff --git a/public/content/translations/tr/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/tr/developers/docs/smart-contracts/formal-verification/index.md index bfa95db888e..4a6a5f19f99 100644 --- a/public/content/translations/tr/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/tr/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ Düşük düzeyli resmi spesifikasyonlar Hoare tarzı özellikler veya yürütme ### Hoare tarzı özellikler {#hoare-style-properties} -[Hoare Mantığı](https://en.wikipedia.org/wiki/Hoare_logic), akıllı sözleşmeleri de kapsayan programların doğruluğu hakkında resmi bir gerekçelendirme kural sınıfı sağlar. Hoare-tarzı bir özellik, Hoare üçlüsü tarafından temsil edilir \{_P_}_c_\{_Q_}, burada _c_ bir programdır ve _P_ ile _Q_ da _c_ (yani program) durumuna yönelik ifadelerdir, resmi olarak sırayla _ön koşullar_ ve _art koşullar_ olarak tanımlanmışlardır. +[Hoare Mantığı](https://en.wikipedia.org/wiki/Hoare_logic), akıllı sözleşmeleri de kapsayan programların doğruluğu hakkında resmi bir gerekçelendirme kural sınıfı sağlar. Hoare-tarzı bir özellik, Hoare üçlüsü tarafından temsil edilir `{P}c{Q}`, burada `c` bir programdır ve `P` ile `Q` da `c` (yani program) durumuna yönelik ifadelerdir, resmi olarak sırayla _ön koşullar_ ve _art koşullar_ olarak tanımlanmışlardır. Bir ön koşul, bir fonksiyonun doğru yürütülmesi için gerekli koşulları açıklayan bir ifadedir; bu sözleşmeyi çağıran kullanıcılar bu gerekliliği karşılamak zorundadır. Bir art koşul ise doğru biçimde yürütülmesi şartıyla bir fonksiyonun tesis ettiği koşulu açıklayan bir ifadedir; kullanıcılar, fonksiyona çağrı sonrası bu koşulun doğru olmasını bekler. Hoare mantığındaki bir _değişmez_, fonksiyonun yürütülmesi ile korunan bir ifadedir (örneğin, değişmez). diff --git a/public/content/translations/zh-tw/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/zh-tw/developers/docs/smart-contracts/formal-verification/index.md index 99c23dec263..35f166e2d69 100644 --- a/public/content/translations/zh-tw/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/zh-tw/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: zh-tw ### 霍爾式屬性 {#hoare-style-properties} -[霍爾邏輯](https://en.wikipedia.org/wiki/Hoare_logic)提供了一套形式化規則，用於推理包括智慧型合約等程式的正確性。 霍爾式屬性使用霍爾三元組 \{_P_}_c_\{_Q_} 表示，其中 _c_ 是一個程式，_P_ 和 _Q_ 為_c_（即程式）的狀態述詞，正式描述分別為_前置條件_和_後置條件_。 +[霍爾邏輯](https://en.wikipedia.org/wiki/Hoare_logic)提供了一套形式化規則，用於推理包括智慧型合約等程式的正確性。 霍爾式屬性使用霍爾三元組 `{P}c{Q}` 表示，其中 `c` 是一個程式，`P` 和 `Q` 為`c`（即程式）的狀態述詞，正式描述分別為_前置條件_和_後置條件_。 前置條件是描述正確執行函式所需條件的述詞；叫用合約的使用者必須滿足該要求。 後置條件是描述函式正確執行時所建立之條件的述詞；使用者在叫用函式後可以預計該條件為 true。 在霍爾邏輯中，_不變量_是指透過執行函式保留的述詞（即，它不會改變）。 diff --git a/public/content/translations/zh/developers/docs/smart-contracts/formal-verification/index.md b/public/content/translations/zh/developers/docs/smart-contracts/formal-verification/index.md index 642a316f529..5a2096aae15 100644 --- a/public/content/translations/zh/developers/docs/smart-contracts/formal-verification/index.md +++ b/public/content/translations/zh/developers/docs/smart-contracts/formal-verification/index.md @@ -70,7 +70,7 @@ lang: zh ### 霍尔式属性 {#hoare-style-properties} -[霍尔逻辑](https://en.wikipedia.org/wiki/Hoare_logic)提供了一套形式化规则来推理程序（包括智能合约）的正确性。 霍尔式属性使用霍尔三元组 \{_P_}_c_\{_Q_} 表示，其中 _c_ 代表程序，_P_ 和 _Q_ 是 _c_（即程序）状态的谓词，它们正式描述成_前置条件_和_后置条件_。 +[霍尔逻辑](https://en.wikipedia.org/wiki/Hoare_logic)提供了一套形式化规则来推理程序（包括智能合约）的正确性。 霍尔式属性使用霍尔三元组 `{P}c{Q}` 表示，其中 `c` 代表程序，`P` 和 `Q` 是 `c`（即程序）状态的谓词，它们正式描述成_前置条件_和_后置条件_。 前置条件是描述函数正确执行所需条件的谓词；用户调用合约必须满足该要求。 后置条件是描述函数在正确执行时所达成条件的谓词；用户在调用函数后可以期待该条件为真。 在霍尔逻辑中，_不变量_是一个在函数执行时保留的谓词（即它不改变）。