ethereum · wackerow · Mar 21, 2025 · Mar 19, 2025 · Mar 21, 2025 · Mar 21, 2025
@@ -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).
 

@@ -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 είναι μια πρόταση που διατηρείται με εκτέλεση συνάρτησης (δηλαδή, δεν αλλάζει).
 

@@ -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).
 

@@ -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 (یعنی برنامه) هستند که به ترتیب به صورت _پیش شرط‌ها_ و _پس شرط‌ها_ توصیف می‌شوند.
 
 پیش شرط یک گزاره است که شرایط لازم برای اجرای صحیح یک تابع را توصیف می کند. کاربرانی که قرارداد را امضا می کنند باید این شرط را برآورده کنند. پیش شرط یک گزاره است که شرایط لازم برای اجرای صحیح یک تابع را توصیف می کند. کاربرانی که قرارداد را امضا کنند باید این شرط را تعیین کنند. یک _ثابت_ در منطق هوآر یک گزاره است که توسط اجرای یک تابع حفظ می‌شود (یعنی تغییر نمی‌کند).
 

@@ -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).
 

@@ -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` (यानी, कार्यक्रम) की स्थिति पर विधेय हैं, औपचारिक रूप से क्रमशः _प्रीकंडीशंस_ और _पोस्टकंडीशन_ के रूप में वर्णित हैं।
 
 एक पूर्व शर्त एक विधेय है जो किसी फ़ंक्शन के सही निष्पादन के लिए आवश्यक शर्तों का वर्णन करता है; अनुबंध में कॉल करने वाले उपयोगकर्ताओं को इस आवश्यकता को पूरा करना होगा। एक पोस्टकंडीशन एक विधेय है जो उस स्थिति का वर्णन करता है जिससे एक फ़ंक्शन लागू होता है अगर सही ढंग से लागू किया जाता है; उपयोगकर्ता फ़ंक्शन में कॉल करने के बाद इस स्थिति के सत्य होने की उम्मीद कर सकते हैं। होरे लॉजिक में एक _इनवेरिएंट_ एक विधेय है जिसे किसी फ़ंक्शन के निष्पादन द्वारा संरक्षित किया जाता है (यानी, यह नहीं बदलता है)।
 

@@ -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).
 

@@ -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).
 

@@ -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の状態についての述語です。
 
 事前条件は関数を正しく実行するために求められる条件を表しています。スマートコントラクトを呼び出す際には、この事前条件が満たされている必要があります。 事後条件は、関数が正しく実行された場合に成立する条件を表しています。関数呼び出しの後はこの事後条件が真となることが期待されます。 ホーア論理の_不変条件_は、関数の実行中は常に維持されます(すなわち、変化しません)。
 

@@ -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).