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

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

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

Δείτε επίσης

• Αλγεβρική σημασιολογία — με όρους αλγεβρών
• Δηλωτική σημασιολογία — μέσω της μετάφρασης ενός προγράμματος σε μια άλλη γλώσσα
• Λειτουργική σημασιολογία — με όρους της κατάστασης του υπολογισμού
• Τυπική σημασιολογία των γλωσσών προγραμματισμού — γενικά
• Σημασιολογία κατηγορηματικού μετασχηματισμού (Predicate transformer semantics) — περιγράφει τη σημασία ενός τμήματος ενός προγράμματος σαν τη συνάρτηση που μετασχηματίζει μια μετασυνθήκη (postcondition) στην προσυνθήκη (precondition) που ήταν προϋπόθεση αυτής.