Ποια είναι η διαφορά μεταξύ της ολικής ορθότητας και της μερικής ορθότητας;


Απάντηση 1:

Μια συνολική προδιαγραφή ορθότητας είναι επίσης μια μερική προδιαγραφή ορθότητας. Η μερική ορθότητα είναι ασθενέστερη επειδή χρειάζεται την πρόσθετη βοήθεια των τερματικών S για να φτάσει στο συμπέρασμα: Το R κρατάει στην τελική κατάσταση.

Για μια μερική προδιαγραφή ορθότητας {Q} S {R}, μπορείτε να λάβετε τις ακόλουθες πληροφορίες: Λαμβάνοντας υπόψη μια κατάσταση εκκίνησης που ικανοποιεί το Q, το S μπορεί να τερματίσει ή όχι. Αν τερματίσει το S, μετά την εκτέλεση του S, θα φτάσετε σε μια τελική κατάσταση που ικανοποιεί το R. Αν όχι, το R είναι άχρηστο αφού δεν υπάρχει τελική κατάσταση.

Για παράδειγμα:

{x == 10}
ενώ (y! = 0):
    y = y - 1
x = 0
{x == 0}

Πρόκειται για μια μερική περιγραφή της ορθότητας. Αν το y αρχικοποιηθεί με κάποιο αριθμό ίσο ή μεγαλύτερο από 0, το S τερματίζεται και μετά από αυτό το x είναι 0. Αν και το y ξεκινά με αρνητικό αριθμό, το S θα βρεθεί για πάντα και αφού δεν τερματίσει, μετά την εκτέλεση του S ».

Πράγματι, το R μπορεί να είναι οτιδήποτε εάν το S είναι ένας dead-loop. Για παράδειγμα, για κάθε Q και R:

{Q}
ενώ (αλήθεια):
    y = y - 1
{R}

είναι πάντα μια μερική προδιαγραφή ορθότητας.

Αν το Q δεν είναι αρκετά ισχυρό, δεν μπορείς να εγγυηθείς τον τερματισμό του S, πόσο μάλλον λόγος για την κατάσταση μετά την εκτέλεση του S. Σε αυτή την περίπτωση μπορείτε να προσθέσετε μη αυτόματα μια συνθήκη: το S τερματίζει. Με το Q και αυτό, η συλλογιστική μπορεί να συνεχιστεί.

Για το σύνολο των προδιαγραφών ορθότητας {Q} S {R}, το Q είναι αρκετά ισχυρό για να εξασφαλίσει τον τερματισμό του S, έτσι μπορείτε να συμπεράνετε ότι το S θα τερματιστεί και η τελική κατάσταση θα ικανοποιήσει R.

Για παράδειγμα:

{x == 10}
ενώ (x! = 0):
    x = χ - 1
{x == 0}

είναι μια συνολική προδιαγραφή ορθότητας.

BTW: Δεν είμαι σίγουρος αν η απάντηση είναι σωστή επειδή η ερώτηση έχει επισημανθεί με πολιτική ορθότητα. Ενώ ο ορισμός στην ερώτηση μοιάζει ακριβώς με τον ορισμό της Πληροφορικής.