Γλώσσα προδιαγραφών
| Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. |
Μια γλώσσα προδιαγραφών (specification language) είναι μια τυπική γλώσσα που χρησιμοποιείται στην επιστήμη των υπολογιστών. Σε αντίθεση με τις περισσότερες γλώσσες προγραμματισμού, οι οποίες είναι απευθείας εκτελέσιμες τυπικές γλώσσες που χρησιμοποιούνται για την υλοποίηση ενός συστήματος, οι γλώσσες προδιαγραφών χρησιμοποιούνται κυρίως κατά τη διάρκεια της ανάλυσης συστημάτων (systems analysis), της ανάλυσης απαιτήσεων (requirements analysis) και της σχεδίασης συστημάτων (systems design).
Οι γλώσσες προδιαγραφών γενικά δεν εκτελούνται κατευθείαν. Περιγράφουν ένα σύστημα σε αρκετά υψηλότερο επίπεδο σε σχέση με μια γλώσσα προγραμματισμού. Στην πραγματικότητα, θεωρείται λάθος αν μια προδιαγραφή απαιτήσεων περιλαμβάνει λεπτομέρειες της υλοποίησης που δε χρειάζονται, γιατί οι προδιαγραφές πρέπει να περιγράφουν τι και όχι πώς.
Μια κοινή βασική παραδοχή πολλών προσεγγίσεων προδιαγραφής είναι ότι τα προγράμματα μοντελοποιούνται σαν αλγεβρικές ή μοντελο-θεωρητικές δομές που περιλαμβάνουν μια συλλογή από σύνολα τιμών δεδομένων μαζί με συναρτήσεις πάνω σε αυτά τα σύνολα. Αυτό το επίπεδο αφαίρεσης αντιστοιχεί στην άποψη ότι η ορθότητα της συμπεριφοράς εισόδου-εξόδου ενός προγράμματος είναι πιο σημαντική από τις υπόλοιπες ιδιότητές του.
Στην προδιαγραφή με βάση τις ιδιότητες (property-oriented), η οποία για παράδειγμα ακολουθείται από την CASL, οι προδιαγραφές των προγραμμάτων αποτελούνται κυρίως από λογικά αξιώματα, συνήθως σε ένα λογικό σύστημα, στο οποίο η ισότητα έχει κυρίαρχο ρόλο. Με αυτόν τον τρόπο περιγράφονται οι ιδιότητες που πρέπει να ικανοποιούν οι συναρτήσεις - συχνά απλά μόνο μέσω των σχέσεων μεταξύ τους. Αυτό έρχεται σε αντίθεση με την αποκαλούμενη μοντελο-θεωρητική προδιαγραφή σε θεωρίες όπως η VDM και ο συμβολισμός Z (Z notation), που αποτελούνται από μια απλή εκδοχή της απαιτούμενης συμπεριφοράς.
Οι προδιαγραφές μπορεί να υπόκεινται στη διαδικασία της εκλέπτυνσης (refinement), όπου συμπληρώνονται διαδοχικά οι λεπτομέρειες μέχρι το επίπεδο της υλοποίησης. Το αποτέλεσμα μιας τέτοιας διαδικασίας εκλέπτυνσης είναι ένας εκτελέσιμος αλγόριθμος, ο οποίος μπορεί να διατυπωθεί είτε σε μια γλώσσα προγραμματισμού, είτε στο εκτελέσιμο υποσύνολο της γλώσσας προδιαγραφής που ήδη χρησιμοποιείται. Για παράδειγμα, οι διοχετεύσεις Χάρτμαν (Hartmann pipelines), όταν εφαρμόζονται σωστά, μπορούν να θεωρηθούν προδιαγραφή ροής δεδομένων (dataflow), η οποία είναι άμεσα εκτελέσιμη. Ένα άλλο παράδειγμα είναι το μοντέλο Actor, το οποίο δεν έχει καθόλου περιεχόμενο εφαρμογής και πρέπει να εξειδικεύεται για να μπορεί να εκτελεστεί.
Μια σημαντική χρήση των γλωσσών προδιαγραφών είναι η δυνατότητα δημιουργίας μαθηματικών αποδείξεων ορθότητας προγράμματος, μέσω ενός αποδείκτη θεωρημάτων (theorem prover).
Γλώσσες Επεξεργασία
- CASL
- VDM
- Συμβολισμός Z (Z Notation)
- LePUS3 (οπτική, αντικειμενοστρεφής γλώσσα περιγραφής σχεδίασης)
- Perfect