fix build errors

Author: corwintines

public/content/translations/el/developers/docs/smart-contracts/formal-verification/index.md

@@ -50,15 +50,15 @@ lang: el
 
 ### Προδιαγραφές υψηλού επιπέδου {#high-level-specifications}
 
-Όπως υποδηλώνει το όνομα, μια προδιαγραφή υψηλού επιπέδου (που ονομάζεται επίσης «προδιαγραφή προσανατολισμένη στο μοντέλο») περιγράφει τη συμπεριφορά υψηλού επιπέδου ενός προγράμματος. Οι προδιαγραφές υψηλού επιπέδου μοντελοποιούν ένα έξυπνο συμβόλαιο ως μια [πεπερασμένη κατάσταση μηχανής](https://en.wikipedia.org/wiki/Finite-state_machine) (FSM), η οποία μπορεί να μεταβεί μεταξύ καταστάσεων εκτελώντας λειτουργίες, με τη χρονική λογική να χρησιμοποιείται για τον ορισμό τυπικών ιδιοτήτων για το μοντέλο FSM.
+Όπως υποδηλώνει το όνομα, μια προδιαγραφή υψηλού επιπέδου (που ονομάζεται επίσης "προδιαγραφή προσανατολισμένη στο μοντέλο") περιγράφει τη συμπεριφορά υψηλού επιπέδου ενός προγράμματος. Οι προδιαγραφές υψηλού επιπέδου μοντελοποιούν ένα έξυπνο συμβόλαιο ως μια [πεπερασμένη κατάσταση μηχανής](https://en.wikipedia.org/wiki/Finite-state_machine) (FSM), η οποία μπορεί να μεταβεί μεταξύ καταστάσεων εκτελώντας λειτουργίες, με τη χρονική λογική να χρησιμοποιείται για τον ορισμό τυπικών ιδιοτήτων για το μοντέλο FSM.
 
-Οι [χρονικές λογικές](https://en.wikipedia.org/wiki/Temporal_logic) είναι «κανόνες για τον συλλογισμό σχετικά με προτάσεις που προσδιορίζονται ως προς το χρόνο (π.χ. «_Πάντα_ πεινάω» ή «_Τελικά_ θα πεινάσω»).» Όταν εφαρμόζονται στην τυπική επαλήθευση, οι χρονικές λογικές χρησιμοποιούνται για να δηλώσουν ισχυρισμούς σχετικά με τη σωστή συμπεριφορά συστημάτων που μοντελοποιούνται ως μηχανές κατάστασης. Ειδικότερα, μια χρονική λογική περιγράφει τις μελλοντικές καταστάσεις στις οποίες μπορεί να βρίσκεται ένα έξυπνο συμβόλαιο και πώς μεταβαίνει μεταξύ των καταστάσεων.
+Οι [χρονικές λογικές](https://en.wikipedia.org/wiki/Temporal_logic) είναι "κανόνες για τον συλλογισμό σχετικά με προτάσεις που προσδιορίζονται ως προς το χρόνο (π.χ. '_Πάντα_ πεινάω' ή '_Τελικά_ θα πεινάσω')." Όταν εφαρμόζονται στην τυπική επαλήθευση, οι χρονικές λογικές χρησιμοποιούνται για να δηλώσουν ισχυρισμούς σχετικά με τη σωστή συμπεριφορά συστημάτων που μοντελοποιούνται ως μηχανές κατάστασης. Ειδικότερα, μια χρονική λογική περιγράφει τις μελλοντικές καταστάσεις στις οποίες μπορεί να βρίσκεται ένα έξυπνο συμβόλαιο και πώς μεταβαίνει μεταξύ των καταστάσεων.
 
 Οι προδιαγραφές υψηλού επιπέδου γενικά καταγράφουν δύο κρίσιμες χρονικές ιδιότητες για τα έξυπνα συμβόλαια: **ασφάλεια** και **ζωντάνια**. Οι ιδιότητες ασφάλειας αντιπροσωπεύουν την ιδέα ότι «τίποτα κακό δε συμβαίνει ποτέ» και συνήθως εκφράζουν αμετάβλητες καταστάσεις. Μια ιδιότητα ασφάλειας μπορεί να ορίζει γενικές απαιτήσεις λογισμικού, όπως την αποφυγή [αδιεξόδου](https://www.techtarget.com/whatis/definition/deadlock) ή να εκφράζει συγκεκριμένες ιδιότητες για συμβόλαια (π.χ. αμετάβλητα στοιχεία για τον έλεγχο πρόσβασης σε συναρτήσεις, επιτρεπτές τιμές μεταβλητών κατάστασης ή συνθήκες για μεταφορές κρυπτοπαραστατικών).
 
-Πάρτε για παράδειγμα αυτή την απαίτηση ασφάλειας που καλύπτει τις συνθήκες για τη χρήση των `transfer()` ή `transferFrom()` σε συμβάσεις κρυπτοπαραστατικών ERC-20: _«Το υπόλοιπο ενός αποστολέα δεν είναι ποτέ χαμηλότερο από το ζητούμενο ποσό κρυπτοπαραστατικών που πρόκειται να σταλεί»_. Αυτή η περιγραφή φυσικής γλώσσας ενός αμετάβλητου στοιχείου συμβολαίου μπορεί να μεταφραστεί σε μια επίσημη (μαθηματική) προδιαγραφή, η εγκυρότητα της οποίας μπορεί στη συνέχεια να ελεγχθεί αυστηρά.
+Πάρτε για παράδειγμα αυτή την απαίτηση ασφάλειας που καλύπτει τις συνθήκες για τη χρήση των `transfer()` ή `transferFrom()` σε συμβάσεις κρυπτοπαραστατικών ERC-20: "_Το υπόλοιπο ενός αποστολέα δεν είναι ποτέ χαμηλότερο από το ζητούμενο ποσό κρυπτοπαραστατικών που πρόκειται να σταλεί_". Αυτή η περιγραφή φυσικής γλώσσας ενός αμετάβλητου στοιχείου συμβολαίου μπορεί να μεταφραστεί σε μια επίσημη (μαθηματική) προδιαγραφή, η εγκυρότητα της οποίας μπορεί στη συνέχεια να ελεγχθεί αυστηρά.
 
-Οι ιδιότητες ζωντάνιας διαβεβαιώνουν ότι «συμβαίνει κάτι που τελικά είναι καλό» και αφορούν την ικανότητα ενός συμβολαίου να σημειώνει πρόοδο μέσα από διαφορετικές καταστάσεις. Ένα παράδειγμα μιας ιδιότητας ζωντάνιας είναι η «ρευστότητα», που αναφέρεται στην ικανότητα ενός συμβολαίου να μεταφέρει τα υπόλοιπά του στους χρήστες κατόπιν αιτήματος. Εάν αυτή η ιδιότητα παραβιαστεί, οι χρήστες δε θα μπορούν να αποσύρουν περιουσιακά στοιχεία που αποθηκεύονται στο συμβόλαιο, όπως συνέβη με το [περιστατικό του πορτοφολιού Parity](https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-wallet.html).
+Οι ιδιότητες ζωντάνιας διαβεβαιώνουν ότι "συμβαίνει κάτι που τελικά είναι καλό" και αφορούν την ικανότητα ενός συμβολαίου να σημειώνει πρόοδο μέσα από διαφορετικές καταστάσεις. Ένα παράδειγμα μιας ιδιότητας ζωντάνιας είναι η "ρευστότητα", που αναφέρεται στην ικανότητα ενός συμβολαίου να μεταφέρει τα υπόλοιπά του στους χρήστες κατόπιν αιτήματος. Εάν αυτή η ιδιότητα παραβιαστεί, οι χρήστες δε θα μπορούν να αποσύρουν περιουσιακά στοιχεία που αποθηκεύονται στο συμβόλαιο, όπως συνέβη με το [περιστατικό του πορτοφολιού Parity](https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-wallet.html).
 
 ### Προδιαγραφές χαμηλού επιπέδου {#low-level-specifications}
 
@@ -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 είναι μια πρόταση που διατηρείται με εκτέλεση συνάρτησης (δηλαδή, δεν αλλάζει).
 
@@ -162,7 +162,7 @@ function safe_add(uint x, uint y) returns(uint z){
 
 Η τυπική επαλήθευση χρησιμοποιείται για να αξιολογήσει τη σωστή λειτουργία κρίσιμων συστημάτων, των οποίων η αποτυχία μπορεί να έχει καταστροφικές συνέπειες, όπως θάνατο, τραυματισμό ή οικονομική καταστροφή. Τα έξυπνα συμβόλαια είναι εφαρμογές υψηλής αξίας που ελέγχουν τεράστιες ποσότητες αξίας και απλά λάθη στον σχεδιασμό μπορούν να οδηγήσουν σε [μη αναστρέψιμες απώλειες για τους χρήστες](https://www.freecodecamp.org/news/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce/amp/). Η τυπική επαλήθευση ενός συμβολαίου πριν τη δημοσίευση, ωστόσο, μπορεί να αυξήσει τις εγγυήσεις ότι θα λειτουργήσει όπως αναμένεται όταν εκτελείται στην αλυσίδα συστοιχιών.
 
-Η αξιοπιστία είναι μια ιδιαίτερα επιθυμητή ποιότητα σε οποιοδήποτε έξυπνο συμβόλαιο, ειδικά επειδή ο κώδικας που αναπτύσσεται στο εικονικό μηχάνημα του Ethereum (EVM) είναι συνήθως αμετάβλητος. Με τις αναβαθμίσεις μετά την κυκλοφορία να μην είναι εύκολα προσβάσιμες, η ανάγκη εγγύησης της αξιοπιστίας των συμβολαίων καθιστά απαραίτητη την τυπική επαλήθευση. Η τυπική επαλήθευση είναι σε θέση να εντοπίσει δύσκολα προβλήματα, όπως υποχείλιση και υπερχείλιση ακεραίων, επανεισδοχή και κακές βελτιστοποιήσεις gas, οι οποίες μπορεί να ξεφύγουν από ελεγκτές και δοκιμαστές.
+Η αξιοπιστία είναι μια ιδιαίτερα επιθυμητή ποιότητα σε οποιοδήποτε έξυπνο συμβόλαιο, ειδικά επειδή ο κώδικας που αναπτύσσεται στο εικονικό μηχάνημα του Ethereum (EVM) είναι συνήθως αμετάβλητος. Με τις αναβαθμίσεις μετά την κυκλοφορία να μην είναι εύκολα προσβάσιμες, η ανάγκη εγγύησης της αξιοπιστίας των συμβολαίων καθιστά απαραίτητη την τυπική επαλήθευση. Η τυπική επαλήθευση είναι σε θέση να εντοπίσει δύσκολα προβλήματα, όπως υποχείλιση και υπερχείλιση ακεραίων, επανεισδοχή και κακές βελτιστοποιήσεις gas, οι οποίες μπορούν να ξεφύγουν από ελεγκτές και δοκιμαστές.
 
 #### Απόδειξη λειτουργικής ορθότητας {#prove-functional-correctness}