Η λογική Hoare είναι ένα επίσημο σύστημα με ένα σύνολο λογικών κανόνων για τον αυστηρό συλλογισμό σχετικά με την ορθότητα των προγραμμάτων υπολογιστών. Προτάθηκε το 1969 από τον Βρετανό επιστήμονα υπολογιστών και λογικό Tony Hoare, και στη συνέχεια βελτιώθηκε από τον Hoare και άλλους ερευνητές.
Τι είναι οι τρίπλες Hoare;
Ένα τριπλό Hoare έχει τρία μέρη, μια προϋπόθεση P, μια δήλωση προγράμματος ή μια σειρά από προτάσεις S και μια μετασυνθήκη Q. Συνήθως γράφεται με τη μορφή. {P} S {Q} Η σημασία είναι "αν το P είναι αληθές πριν από την εκτέλεση του S, και αν η εκτέλεση του S τερματιστεί, τότε το Q είναι αληθές μετά".
Σε τι χρησιμοποιείται η λογική Hoare;
Ο στόχος της λογικής Hoare είναι να παρέχει ένα επίσημο σύστημα συλλογισμού σχετικά με την ορθότητα του προγράμματος. Η λογική Hoare βασίζεται στην ιδέα μιας προδιαγραφής ως σύμβασης μεταξύ της υλοποίησης μιας λειτουργίας και των πελατών της. Η προδιαγραφή αποτελείται από μια προϋπόθεση και μια μετασυνθήκη.
Τι είναι το Hoare;
Το
Hoare είναι ένα αγγλικό επώνυμο που προέρχεται από τη μέση αγγλική γλώσσα hor(e) που σημαίνει γκριζομάλλης ή ασπρομάλλη. Αξιοσημείωτα άτομα με το επώνυμο περιλαμβάνουν: Albert Alfred Hoare, γνωστός ως Bert Hoare (1874–1962), πολιτικός της Νότιας Αυστραλίας. Des Hoare (γεν. 1934), Αυστραλός αθλητής του κρίκετ. … John Gurney Hoare (1810–1875), Άγγλος παίκτης κρίκετ και …
Είναι η λογική Hoare ολοκληρωμένη;
Η απάντηση είναι ναι, και δείχνει ότι η Hoare λογική είναι καλή. Η ευρωστία είναι σημαντική γιατί λέειότι η λογική Hoare δεν μας επιτρέπει να αντλήσουμε ισχυρισμούς μερικής ορθότητας που στην πραγματικότητα δεν ισχύουν. Η απόδειξη της ορθότητας απαιτεί επαγωγή στις παραγώγους στο ⊢ {P} c {Q} (παραλείπουμε αυτήν την απόδειξη).
