Αξιωματική σημασιολογία
 |
Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. |
Αξιωματική σημασιολογία (axiomatic semantics) ονομάζεται μια προσέγγιση της απόδειξης της ορθότητας προγραμμάτων, η οποία βασίζεται στη μαθηματική λογική. Έχει στενή σχέση με τη λογική Χόαρ.
Η αξιωματική σημασιολογία ορίζει τη σημασία μιας εντολής ενός προγράμματος περιγράφοντας την επίδρασή της σε βεβαιώσεις (assertions) σχετικά με την κατάσταση του προγράμματος. Οι βεβαιώσεις είναι λογικές προτάσεις - κατηγορήματα με μεταβλητές, όπου οι μεταβλητές περιγράφουν την κατάσταση του προγράμματος.
Δείτε επίσης
[Επεξεργασία | επεξεργασία κώδικα]- Αλγεβρική σημασιολογία — με όρους αλγεβρών
- Δηλωτική σημασιολογία — μέσω της μετάφρασης ενός προγράμματος σε μια άλλη γλώσσα
- Λειτουργική σημασιολογία — με όρους της κατάστασης του υπολογισμού
- Τυπική σημασιολογία των γλωσσών προγραμματισμού — γενικά
- Σημασιολογία κατηγορηματικού μετασχηματισμού (Predicate transformer semantics) — περιγράφει τη σημασία ενός τμήματος ενός προγράμματος σαν τη συνάρτηση που μετασχηματίζει μια μετασυνθήκη (postcondition) στην προσυνθήκη (precondition) που ήταν προϋπόθεση αυτής.