Τυπική σημασιολογία των γλωσσών προγραμματισμού: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
μΧωρίς σύνοψη επεξεργασίας |
μΧωρίς σύνοψη επεξεργασίας |
||
Γραμμή 5:
Υπάρχουν πολλές προσεγγίσεις στην τυπική σημασιολογία, οι οποίες ανήκουν στις εξής τρεις μεγάλες κλάσεις:
* '''[[Δηλωτική σημασιολογία]]''' ('''Denotational semantics'''), στην οποία κάθε φράση της γλώσσας μεταφράζεται σε μια ''δήλωση'' (''denotation''), δηλ. σε μια φράση σε κάποια άλλη γλώσσα. Η δηλωτική σημασιολογία αντιστοιχεί γενικά στη [[
* '''[[Λειτουργική σημασιολογία]]''' ('''Operational semantics'''), στην οποία η εκτέλεση της γλώσσας περιγράφεται άμεσα (και όχι μέσω μετάφρασης). Η λειτουργική σημασιολογία γενικά αντιστοιχεί στη [[Διερμηνέας (υπολογιστές)|διερμηνεία]], αν και πάλι η "γλώσσα υλοποίησης" του διερμηνέα είναι συνήθως κάποιος μαθηματικός φορμαλισμός. Η λειτουργική σημασιολογία μπορεί να ορίζει κάποια αφηρημένη μηχανή (abstract machine) και να δίνει νόημα σε φράσεις αποδίδοντάς τους τις μεταβάσεις που προκαλούν στις καταστάσεις της μηχανής. Εναλλακτικά, όπως με τον καθαρό [[Λογισμός_λάμδα|λ-λογισμό]], η λειτουργική σημασιολογία μπορεί να οριστεί μέσω συντακτικών μετασχηματισμών σε φράσεις της ίδιας της γλώσσας.
* '''[[Αξιωματική σημασιολογία]]''' ('''Axiomatic semantics'''), η οποία δίνει νόημα σε φράσεις περιγράφοντας τα ''[[λογική|λογικά]] [[αξίωμα|αξιώματα]]'' που εφαρμόζονται σε αυτές. Η αξιωματική σημασιολογία δε διακρίνει μεταξύ του νοήματος μιας φράσης και των λογικών προτάσεων που την περιγράφουν: το νόημά της ''είναι'' ακριβώς ότι μπορεί να αποδειχτεί για αυτή σε κάποια λογική. Το κλασικό παράδειγμα αξιωματικής σημασιολογίας είναι η [[λογική Χόαρ]].
| |||