Αξιωματική σημασιολογία

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

Αξιωματική σημασιολογία (axiomatic semantics) ονομάζεται μια προσέγγιση της απόδειξης της ορθότητας προγραμμάτων, η οποία βασίζεται στη μαθηματική λογική. Έχει στενή σχέση με τη λογική Χόαρ.

Η αξιωματική σημασιολογία ορίζει τη σημασία μιας εντολής ενός προγράμματος περιγράφοντας την επίδρασή της σε βεβαιώσεις (assertions) σχετικά με την κατάσταση του προγράμματος. Οι βεβαιώσεις είναι λογικές προτάσεις - κατηγορήματα με μεταβλητές, όπου οι μεταβλητές περιγράφουν την κατάσταση του προγράμματος.

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Axiomatic semantics της Αγγλόγλωσσης Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).