test.tex

\documentclass{softlab-thesis}


%%%
%%%  The document
%%%

\begin{document}

%%%  Title page

\frontmatter

\title{%
  Μεταγλωττιστής Calvin σε NFlint%
}
\author{%
  Βασίλειος Μ.\ Κουταβάς%
}
\date{%
  Οκτώβριος 2002%
}
\supervisor{%
  Νικόλαος Παπασπύρου, Λέκτορας%
}
\committeemembers{%
  Εμμανουήλ Σκορδαλάκης, Καθηγητής%
\and%
  Ευστάθιος Ζάχος, Καθηγητής%
}
\url{http://www.softlab.ntua.gr/\textasciitilde vkoutav/}
\TRnumber{CSD-SW-TR-2-02}

\maketitle


%%%  Abstract

\begin{abstract}%
\noindent%
Η γλώσσα C καθώς και οι απόγονοί της αποτελούν ένα ισχυρό και
αδιαμφισβήτητο κατεστημένο στη σύγχρονη βιομηχανία λογισμικού.
Πρόκειται για μια πολύ δημοφιλή γλώσσα προγραμματισμού γενικού σκοπού,
που χαρακτηρίζεται από οικονομία στην έκφραση, ένα μεγάλο σύνολο από
τελεστές και τύπους δεδομένων και από την υψηλή μεταφερσιμότητα του
πηγαίου κώδικα. Το τρέχον επίσημο κείμενο αναφοράς για τη γλώσσα C
είναι το διεθνές πρότυπο ISO/IEC 9899:1990. Στο κείμενο αυτό, η
σημασιολογία της C ορίζεται με άτυπο τρόπο χρησιμοποιώντας φυσική
γλώσσα, κάτι που συχνά οδηγεί σε παρερμηνείες.

Σε αυτή τη διατριβή προτείνεται μια τυπική δηλωτική σημασιολογία για τη
γλώσσα προγραμματισμού ANSI~C, με έμφαση στην ακρίβεια και την
πληρότητα ως προς το πρότυπο. Διαφαίνεται ότι μια γλώσσα
προγραμματισμού τόσο χρήσιμη στην πράξη και τόσο εγγενώς πολύπλοκη όσο
η C είναι δυνατό να ορισθεί με τυπικό τρόπο. Η προτεινόμενη
σημασιολογία είναι δυνατό να χρησιμοποιηθεί ως ένα ακριβές, αφηρημένο
και ανεξάρτητο υλοποίησης πρότυπο για τη C. Επιπλέον, μπορεί να
αποτελέσει τη βάση για τη διατύπωση τυπικών συλλογισμών σχετικά με τη
συμπεριφορά των προγραμμάτων σε C, καθώς και ένα πολύτιμο θεωρητικό
εργαλείο στη διαδικασία ανάπτυξης λογισμικού.

Προκειμένου να βελτιωθεί η δόμηση και η κομψότητα της προτεινόμενης
σημασιολογίας, γίνεται χρήση των μονάδων και των μετασχηματιστών
μονάδων για την απεικόνιση διαφορετικών πλευρών της σημασιολογίας των
υπολογισμών. Ενδιαφέροντα ερευνητικά αποτελέσματα έχουν επιτευχθεί στην
προσπάθεια για την ακριβή μοντελοποίηση πολύπλοκων χαρακτηριστικών της
C, όπως η απροσδιόριστη σειρά αποτίμησης των εκφράσεων και τα σημεία
διαδοχής, με τη χρήση μονάδων. Τα αποτελέσματα αυτά είναι χρήσιμα στην
περιγραφή της σημασιολογίας γλωσσών προγραμματισμού που υποστηρίζουν μη
ντετερμινιστικά χαρακτηριστικά και παραλληλισμό.

Μια υλοποίηση ενός αφηρημένου διερμηνέα για προγράμματα C, βασισμένου
στην προτεινόμενη σημασιολογία, έχει επίσης αναπτυχθεί χρησιμοποιώντας
τη Haskell ως γλώσσα υλοποίησης. Η υλοποίηση αυτή χρησιμοποιείται για
την αξιολόγηση της ορθότητας και της πληρότητας της προτεινόμενης
σημασιολογίας. Παρότι η εργασία αυτή βρίσκεται ακόμα σε εξέλιξη, τα ως
τώρα αποτελέσματα είναι ιδιαίτερα ικανοποιητικά.

\begin{keywords}
Γλώσσα προγραμματισμού ANSI~C, πρότυπο ISO/IEC 9899:1990, τυπική
περιγραφή, δηλωτική σημασιολογία, μονάδες, μετασχηματιστές μονάδων.
\end{keywords}
\end{abstract}


%%%  Acknowledgements

\begin{acknowledgements}
Θέλω κατ'~αρχήν να ευχαριστήσω τον επιβλέποντα καθηγητή αυτής της
διατριβής, κ.~Μανόλη Σκορδαλάκη, για τη συνεχή καθοδήγηση και
εμπιστοσύνη του. Καθ'~όλη τη διάρκεια των δέκα ετών της συνεργασίας
μας, ήταν πάντοτε διαθέσιμος όποτε τον χρειαζόμουν, εξυπηρετικός και
φιλικός. Ευχαριστώ επίσης τα μέλη της εξεταστικής επιτροπής,
κ.κ.~Γιώργο Παπακωνσταντίνου, Ανδρέα Σταφυλοπάτη, Στάθη Ζάχο, Παναγιώτη
Τσανάκα, Τίμο Σελλή και Πάνο Ροντογιάννη, για την πρόθυμη και πάντα
αποτελεσματική βοήθειά τους, τις πολύτιμες συμβουλές και τις χρήσιμες
συζητήσεις που είχαμε.

Οι σπουδές μου στο Πανεπιστήμιο Cornell επηρέασαν κατά πολύ τον τρόπο
σκέψης μου αλλά και την κατεύθυνση της έρευνάς μου. Θα ήθελα να
ευχαριστήσω τον επιβλέποντά μου εκεί, κ.~David Gries, καθώς και τα άλλα
μέλη του τμήματος Επιστήμης Υπολογιστών οι οποίοι με δίδαξαν το
συνδυασμό της θεωρίας με την πράξη, με κατεύθυναν προς την τυπική
μελέτη των γλωσσών προγραμματισμού και μου παρείχαν πρόσβαση σε άφθονη
βιβλιογραφία. Μου πήρε κάποιο χρόνο μέχρι να εκτιμήσω όλα αυτά στο
δέοντα βαθμό και αισθάνομαι ότι δεν είχα ακόμα την ευκαιρία να τους
ευχαριστήσω.

Τα μέλη του Εργαστηρίου Τεχνολογίας Λογισμικού ήταν πάντα καλοί φίλοι.
Ιδιαίτερα, θα ήθελα να ευχαριστήσω τους Βασίλη Βεσκούκη, Σίμο Ρετάλη,
Τάσο Κουτουμάνο, Κλειώ Σγουροπούλου και Κώστα Ταβερναράκη για την
εξαιρετική υποστήριξή τους, τις πολλές και όμορφες ώρες συζήτησης που
μοιραστήκαμε. Επίσης, ευχαριστώ τους πολυάριθμους διαχειριστές του
εργαστηρίου για την τεχνική υποστήριξη που ποτέ δε μου αρνήθηκαν όλα
αυτά τα χρόνια.

Πολλές ευχαριστίες οφείλω στο φίλο μου και συνάδελφο Dragan
Ma\'{c}o\v{s} που με εισήγαγε στις μονάδες και έκανε χρήσιμες
παρατηρήσεις σχετικά με αυτή τη διατριβή. Επίσης, ευχαριστώ τους Τάσο
Βίγλα, Βασίλη Παπαδήμο για τη βοήθειά τους στις πρώτες φάσεις
αποσφαλμάτωσης της σημασιολογίας, όπως και τους Άλκη Πολυζώτη, Γιάννη
Σισμάνη, Μάνο Ρενιέρη και Κατερίνα Ποτίκα, για τις προτάσεις τους όσον
αφορά στην υλοποίηση της σημασιολογίας.

Θα ήθελα ακόμα να ευχαριστήσω τους φίλους μου που πάντα μου προσέφεραν
αγάπη, ενθάρρυνση και υποστήριξη. Χάρη σε αυτούς, οι σπουδές μου ήταν
πολύ πιο ευχάριστες. Τέλος, ευχαριστώ από βάθους καρδιάς την οικογένειά
μου και τη σύντροφό μου Κατερίνα για την αστείρευτη υπομονή, αγάπη και
εμπιστοσύνη, και γιατί μου επέτρεψαν να απέχω κατά καιρούς από
δραστηριότητες που δε συμβάδιζαν με τις σπουδές μου.

\begin{flushright}
Νικόλαος Σ.\ Παπασπύρου,\\[6pt]
Αθήνα, 27 Φεβρουαρίου 1998.
\end{flushright}

\footacknowledgement{%
  Αυτή η διατριβή τυπώθηκε με το σύστημα προετοιμασίας εγγράφων \LaTeXe,
  χρησιμοποιώντας την κλάση \texttt{thesis} του Wenzel Matiaske. Τα πακέτα
  \texttt{diagrams} και \texttt{QED} του Paul Taylor, για τη δημιουργία
  μεταβατικών διαγραμμάτων και αποδείξεων, ήταν ιδιαίτερα χρήσιμα, όπως
  επίσης και το πακέτο \texttt{semantic} του Peter M{\o}ller Neergaard, για
  τη δημιουργία κανόνων συνεπαγωγής.
}
\end{acknowledgements}


%%%  Various tables

\tableofcontents
\listoftables
\listoffigures


%%%  Main part of the book

\mainmatter

\chapter{Εισαγωγή%
  \label{ch:intro}}

Το κεφάλαιο αυτό είναι μια εισαγωγή στην παρούσα διατριβή. Στην
ενότητα~\ref{sec:intro:c} επιχειρείται μια σύντομη παρουσίαση της
γλώσσας προγραμματισμού C, με έμφαση στην ιστορία και τα χαρακτηριστικά
της. Η ενότητα~\ref{sec:intro:semantics} περιέχει μια περιγραφική
εισαγωγή στη σημασιολογία των γλωσσών προγραμματισμού, προκατειλημμένη
προς την κατεύθυνση της δηλωτικής σημασιολογίας. Η
ενότητα~\ref{sec:intro:overview} είναι μια επισκόπηση αυτής της
διατριβής. Κατ'~αρχήν συζητείται το αντικείμενο, τα κίνητρα και οι
δυνατές εφαρμογές και εν συνεχεία παρουσιάζεται μια επισκόπηση της
μεθοδολογίας που χρησιμοποιείται και μια περίληψη της συνεισφοράς αυτής
της διατριβής. Στην ενότητα~\ref{sec:intro:related} περιέχεται μια
επισκόπηση της συναφούς έρευνας και το κεφάλαιο ολοκληρώνεται με τη
δομή της διατριβής, στην ενότητα~\ref{sec:intro:structure}.


\section{Η γλώσσα προγραμματισμού C%
  \label{sec:intro:c}}

Η C είναι μια ευρύτατα γνωστή και πολύ δημοφιλής γλώσσα προγραμματισμού
γενικού σκοπού. Αναπτύχθηκε κατά τη διάρκεια της περιόδου 1969-1973 στα
εργαστήρια AT\&T Bell Labs ως μια γλώσσα υλοποίησης για το λειτουργικό
σύστημα Unix. Πατέρας της C είναι ο Dennis Ritchie, ο οποίος επίσης
ανέπτυξε τον πρώτο μεταγλωττιστή στην περίοδο 1971-1973. Ένας
λεπτομερής απολογισμός της εξέλιξης της γλώσσας C, γραμμένος από τον
ίδιο τον Dennis Ritchie, βρίσκεται στο \cite{ritchie-1993-dcl}.

Ο άμεσος πρόγονος της C είναι μια γλώσσα που ονομάζεται
B \cite{johnson-1973-plb}, η οποία σχεδιάσθηκε από τον Ken Thompson την
περίοδο 1969-1970 ως μια γλώσσα υλοποίησης για τον υπολογιστή DEC
PDP-7. Η B μπορεί να θεωρηθεί ένα υποσύνολο της
BCPL \cite{richards-1979-blc}, μια γλώσσα που σχεδιάσθηκε από τον
Martin Richards στα μέσα της δεκαετίας του 1960 κυρίως ως ένα εργαλείο
για την ανάπτυξη μεταγλωττιστών. Η κύρια διαφορά ανάμεσα στη C και τους
προγόνους της είναι η παρουσία ενός μη τετριμμένου συστήματος τύπων. Οι
BCPL και B δε διαθέτουν άλλους τύπους πλήν του ``word'', ο οποίος
αναπαριστά συγχρόνως δεδομένα και ``δείκτες'' σε δεδομένα. Η εισαγωγή
νέων τύπων στη C ήταν απαραίτητη προκειμένου να παρέχεται γλωσσική
υποστήριξη των χαρακτήρων και των αριθμών κινητής υποδιαστολής που
είχαν ήδη κάνει την εμφάνισή τους στις αρχές της δεκαετίας του 1970. Το
1973, ο πυρήνας της C όπως την ξέρουμε σήμερα είχε συμπληρωθεί και ένας
μεταγλωττιστής για τον DEC PDP-11 είχε ήδη αναπτυχθεί από τον Dennis
Ritchie. Η γλώσσα υποστήριζε ακεραίους και χαρακτήρες ως βασικούς
τύπους, πλήρεις τύπους πινάκων και δεικτών, ειδικούς λογικούς τελεστές
και έναν ισχυρό προεπεξεργαστή.

Στα χρόνια που ακολούθησαν, αρκετές αλλαγές εισήχθησαν στη γλώσσα C
λόγω των αυξημένων απαιτήσεων για μεταφερσιμότητα και ασφάλεια. Αρκετοί
νέοι τύποι προστέθησαν στο σύστημα τύπων, καθώς και μετατροπές μεταξύ
τύπων. Η πρώτη ευρέως διαθέσιμη περιγραφή της γλώσσας, το βιβλίο ``The
C Programming Language'' επίσης γνωστό ως ``K\&R'', εμφανίσθηκε το
1978 \cite{kernighan-1978-cpl}.\footnote{Η δεύτερη έκδοση αυτού του
βιβλίου, που περιέχει μεταγενέστερες αλλαγές, εκδόθηκε δέκα χρόνια
αργότερα \cite{kernighan-1988-cpl}. Το βιβλίο ``K\&R'' χρησίμευσε ως
κείμενο αναφοράς για τη γλώσσα ως το 1989, όταν υιοθετήθηκε ένα επίσημο
πρότυπο.} Μέχρι τότε, ο πυρήνας του λειτουργικού συστήματος Unix είχε
γραφεί σε C και τόσο η ίδια η γλώσσα όσο και οι μεταγλωττιστές είχαν
κερδίσει σημαντικά σε εμπιστοσύνη. Κατά τη διάρκεια της δεκαετίας του
1980, η χρήση της γλώσσας C γνώρισε μεγάλη διάδοση και άρχισαν να
διατίθενται μεταγλωττιστές σχεδόν για κάθε τύπο υπολογιστή και
λειτουργικό σύστημα.

Η C, καθώς και οι δυο πρόγονοί της B και BCPL, ανήκει στην οικογένεια
των γλωσσών που εκφράζουν το παραδοσιακό διαδικασιακό μοντέλο
προγραμματισμού, χαρακτηριστικό παράδειγμα του οποίου είναι οι γλώσσες
Fortran και Algol~60. Είναι ιδιαίτερα προσανατολισμένη προς τον
προγραμματισμό συστημάτων και η μικρή και συνοπτική περιγραφή της
επιτρέπει την εύκολη ανάπτυξη απλών μεταγλωττιστών. Η C χαρακτηρίζεται
κυρίως από οικονομία έκφρασης, που υλοποιείται μέσω της λακωνικής
σύνταξης και του μεγάλου πλήθους τελεστών και τύπων δεδομένων, καθώς
επίσης και από το γεγονός ότι επιτρέπει πρόσβαση στα ενδότερα του
υπολογιστή.

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

Σύμφωνα με τον Dennis Ritchie, τα στοιχεία που χαρακτηρίζουν
περισσότερο τη C και τη διαφοροποιούν από τους προγόνους της και άλλες
σύγχρονές της γλώσσες είναι δυο: η στενή σχέση μεταξύ πινάκων και
δεικτών και η σύνταξη των δηλώσεων, που μιμείται αυτή των εκφράσεων.
Όμως, αυτά είναι επίσης ανάμεσα στα πλέον αμφιλεγόμενατα χαρακτηριστικά
της γλώσσας, καθώς και πηγές παρερμηνειών, όχι μόνο για τους αρχάριους
αλλά ακόμα και για έμπειρους προγραμματιστές.

Ως το 1982, οι αλλαγές που εισήχθησαν στη γλώσσα C ως αποτέλεσμα
προσαρμογής αυτής στην καθιερωμένη πρακτική ήταν πολλές. Κάθε
μεταγλωττιστής υλοποιούσε μια ελαφρώς διαφορετική έκδοση της C. Η πρώτη
έκδοση του ``K\&R'' δεν περιέγραφε πια τη γλώσσα όπως αυτή
χρησιμοποιείτο στην πράξη ή, ακόμα και όταν το έκανε, δεν ήταν αρκετά
σαφές σε πολλά σημεία. Σε μια προσπάθεια για την προτυποποίηση της C,
το Αμερικανικό Εθνικό Ινστιτούτο Προτύπων (American National Standards
Institute, ANSI) ίδρυσε την επιτροπή X3J11 το καλοκαίρι του 1983.
Σκοπός της ήταν ``να αναπτύξει ένα καθαρό, συνοπτικό και μη διφορούμενο
πρότυπο για τη γλώσσα προγραμματισμού C, που να κωδικοποιεί τον κοινό,
υπάρχοντα ορισμό της γλώσσας και να προάγει τη μεταφερσιμότητα των
προγραμμάτων μεταξύ περιβαλλόντων της γλώσσας C''. Η επιτροπή ήταν πολύ
προσεκτική και συντηρητική σχετικά με επεκτάσεις της γλώσσας. Η βασική
αλλαγή που υιοθετήθηκε ήταν η χρήση πρωτοτύπων συναρτήσεων, που
αποτελούσε ένα σημαντικό βήμα στην κατεύθυνση προς ένα ισχυρότερο
σύστημα τύπων για τη C. Όμως, η επιτροπή αποφάσισε να επιτρέψει τον
παλαιό τρόπο δήλωσης συναρτήσεων, ως ένα είδος συμβιβασμού με το μεγάλο
όγκο υπάρχοντος λογισμικού σε C.

Η διαδικασία αυτή ολοκληρώθηκε στο τέλος του 1989 και είχε ως
αποτέλεσμα το πρότυπο ANS~X3.159-1989 \cite{ansi-1989-ansisplc}, το
οποίο αργότερα υιοθετήθηκε από το Διεθνή Οργανισμό Προτυποποίησης
(International Organization for Standardization) με κωδικό αριθμό
ISO/IEC 9899:1990 \cite{ansi-1990-plc}. Το πρότυπο συμπληρώνεται από
μια σειρά άλλων εγγράφων που έχουν τη θέση
επεξηγήσεων \cite{ansi-1989-ransisplc} ή
διορθώσεων \cite{ansi-1994-plctc1}. Η έκδοση της γλώσσας C που
προδιαγράφεται στο πρότυπο ονομάζεται ISO C, ή συνήθως ANSI C. Από το
1990 έχει ξεκινήσει μια διαδικασία επανεξέτασης του προτύπου, που
αναμένεται να οδηγήσει σε ένα εντελώς αναμορφωμένο πρότυπο, με το
παρωνύμιο ``C9X'', ως το τέλος του 1999.

Από τα πρώτα χρόνια της ανάπτυξής της, η C έχει χρησιμοποιηθεί για τον
προγραμματισμό μιας ευρείας περιοχής εφαρμογών, συμπεριλαμβανομένου και
του μεγαλύτερου μέρους του λειτουργικού συστήματος Unix. Μεταγλωττιστές
για τη C είναι σήμερα διαθέσιμοι σχεδόν για κάθε σύστημα υπολογιστή
και, παρότι η γλώσσα επιτρέπει ακόμα την ανάπτυξη μη μεταφέρσιμων
εφαρμογών, τα προγράμματα σε C είναι γενικά μεταφέρσιμα, ενίοτε με
μικρές μετατροπές. Κατά τη διάρκεια των τελευταίων είκοσι ετών, η C
έχει χρησιμοποιηθεί ως βάση, ή τουλάχιστον έχει σημαντικά επηρεάσει την
ανάπτυξη αρκετών νέων γλωσσών προγραμματισμού. Μεταξύ αυτών, αξίζει να
αναφέρει κανείς τις Concurrent C \cite{gehani-1989-cc}, Objective
C \cite{cox-1991-oopea} και ιδιαίτερα τις
C++ \cite{stroustrup-1991-cpl, ellis-1990-acrm} και
Java \cite{gosling-1996-jls}. Στη σύγχρονη βιομηχανία λογισμικού μπορεί
να ισχυρισθεί κανείς ότι η C και οι απόγονοί της αποτελούν ένα ισχυρό
και αδιαμφισβήτητο κατεστημένο. Το πρότυπο της γλώσσας είναι σήμερα
αποδεκτό ως μια κοινή βάση για τη C και χρησιμοποιείται ως σημείο
αναφοράς από τους κατασκευαστές αλλά και τους χρήστες υλοποιήσεων και
άλλων εργαλείων.


\section{Σημασιολογία γλωσσών προγραμματισμού%
  \label{sec:intro:semantics}}

Η μελέτη των γλωσσών προγραμματισμού απαρεγκλίτως διακρίνει δυο βασικά
στοιχεία: τη \emph{σύνταξη} (syntax) και τη \emph{σημασιολογία}
(semantics). Η σύνταξη αναφέρεται στην μορφή και τη δομή των καλώς
σχηματισμένων προτάσεων της γλώσσας, συμπεριλαμβανομένων και των
προγραμμάτων. Η σημασιολογία αναφέρεται στην απόδοση ερμηνείας σε αυτές
τις προτάσεις, την οποία πρέπει να σέβονται οι μεταγλωττιστές και οι
άλλες υλοποιήσεις της γλώσσας. Η διαχωριστική γραμμή μεταξύ σύνταξης
και σημασιολογίας δεν είναι πάντοτε καλά ορισμένη. Η ετυμολογία της
λέξης ``σημασιολογία'' (τόσο στα ελληνικά όσο και στα αγγλικά) οδηγεί
στο ρήμα της αρχαίας ελληνικής γλώσσας ``σημαίνω''. Η αρχική σημασία
της λέξης είναι η μελέτη της σύνδεσης μεταξύ των λέξεων και προτάσεων
μιας γλώσσας και της ερμηνείας τους.

Η σύνταξη των γλωσσών προγραμματισμού ορίζεται συνήθως με τυπικό τρόπο.
Αυτή η ερευνητική περιοχή έχει εκτεταμμένα μελετηθεί και υπάρχει σήμερα
πληθώρα αποδεκτών φορμαλισμών. Ο ευρύτερα γνωστός από αυτούς είναι οι
γραμματικές χωρίς συμφραζόμενα, που συνήθως εκφράζονται με τη μορφή
Backus Naur Form (BNF) και παραλλαγές αυτής. Οι γραμματικές επιτρέπουν,
ή και προτείνουν, μια άμεση σύνδεση μεταξύ της σύνταξης και της
υλοποίησης συντακτικών αναλυτών, και αυτή η ισχυρή σύνδεση είναι
πιθανώς ο κυριότερος λόγος που η περιοχή του τυπικού ορισμού της
σύνταξης έχει αναπτυχθεί τόσο πολύ.

Από την άλλη πλευρά, η σημασιολογία των γλωσσών προγραμματισμού
ορίζεται συνήθως με άτυπο τρόπο. Αυτό οφείλεται κυρίως στην
πολυπλοκότητα του εγχειρήματος, που γίνεται ακόμα μεγαλύτερη αν κανείς
αναλογισθεί ότι η απλότητα της μορφής BNF αποδίδεται μερικά στο γεγονός
ότι τα πολυπλοκότερα τμήματα της περιγραφής της σύνταξης έχουν
``μεταφερθεί στο επίπεδο της σημασιολογίας''. Σε αντίθεση με τη σύνταξη
δεν υπάρχουν καθιερωμένοι, σε αποδοχή και σε χρήση, φορμαλισμοί και
μεθοδολογίες για την περιγραφή της σημασιολογίας.

Καθένας που χρησιμοποιεί μια γλώσσα προγραμματισμού για την ανάπτυξη
λογισμικού πρέπει να έχει αντίληψη της σημασιολογίας της γλώσσας σε
κάποιο επίπεδο αφαίρεσης. Οι προγραμματιστές συνήθως αντιλαμβάνονται τη
σημασιολογία μέσω παραδειγμάτων, διαίσθησης και περιγραφών σε φυσική
γλώσσα. Τέτοιες περιγραφές της σημασιολογίας είναι άτυπες και
βασίζονται συνήθως σε ένα πλήθος υποθέσεων σχετικά με τις γνώσεις και
την ικανότητα αντίληψης των αναγνωστών τους. Οι άτυπες περιγραφές είναι
εγγενώς διφορούμενες, όπως συμβαίνει πάντα στην περίπτωση των φυσικών
γλωσσών. Στη καλύτερη περίπτωση, η διαίσθηση του προγραμματιστή
καλύπτει τα σημεία που λείπουν και οδηγεί στη σωστή κατανόηση της
σημασιολογίας. Στη χειρότερη περίπτωση, η περιγραφή είναι μοιραία
διφορούμενη, ή ακόμα και παραπλανητική, και ο προγραμματιστής είναι
εκτεθειμένος σε παρερμηνείες που συχνά οδηγούν σε προγραμματιστικά
σφάλματα.

Η έρευνα στην περιοχή της τυπικής σημασιολογίας των γλωσσών
προγραμματισμού άρχισε στη δεκαετία του 1960. Με τη ραγδαία αύξηση στην
πολυπλοκότητα των γλωσσών προγραμματισμού υψηλού επιπέδου, οι ερευνητές
άρχισαν να αναζητούν μια τυπική σημασιολογία βασισμένη σε συστήματα
μαθηματικής λογικής με ακριβείς κανόνες, ως ένα τρόπο να ξεπερασθούν τα
διφορούμενα σημεία και να επέλθει πειθαρχία σε αυτό το πεδίο. Έκτοτε,
το προϊόν περισσότερων από τριάντα ετών έρευνας είναι η διατύπωση και
εκτενής μελέτη πολυάριθμων μεθόδων και φορμαλισμών. Μια εξαιρετική
εισαγωγή στο πεδίο αυτό είναι η \cite{winskel-1993-fspl}, ενώ
η \cite{mitchell-1996-fpl} παρέχει μια εκτενέστερη παρουσίαση των
μεθόδων και της μαθηματικής θεμελίωσης.

Για ιστορικούς λόγους, οι τυπικές περιγραφές σημασιολογίας
κατατάσσονται σε τρεις κύριες κατηγορίες:
\begin{itemize}
%
\item \emph{Λειτουργική σημασιολογία} (operational semantics): Οι
ερμηνείες είναι ακολουθίες από υπολογιστικά βήματα που
πραγματοποιούνται κατά την εκτέλεση των προγραμμάτων. Μια
συστηματικότερη παραλλαγή είναι η δομική λειτουργική σημασιολογία
(structural operational semantics). Μια στοιχειώδης εισαγωγή μπορεί να
βρεθεί στο \cite{hennessy-1990-spleiusos}
%
\item \emph{Δηλωτική σημασιολογία} (denotational semantics): Οι
ερμηνείες είναι μαθηματικά αντικείμενα, συνήθως συναρτήσεις από
εισόδους σε εξόδους. Αυτή η κατηγορία σημασιολογίας κατασκευάζει ρητά
μαθηματικά μοντέλα των γλωσσών προγραμματισμού. Θα συζητηθεί
περισσότερο στη συνέχεια, καθώς είναι η προσέγγιση που ακολουθείται
στην παρούσα διατριβή.
%
\item \emph{Αξιωματική σημασιολογία} (axiomatic semantics): Οι
ερμηνείες εκφράζονται με έμμεσο τρόπο, μέσω λογικών προτάσεων που
περιγράφουν ιδιότητες των προγραμμάτων. Η προσέγγιση αυτή είναι χρήσιμη
γιατι αποσκοπεί άμεσα στην υποστήριξη της επαλήθευσης των προγραμμάτων.
Η θεμελιώδης εργασία στην περιοχή της αξιωματικής σημασιολογίας είναι
η \cite{hoare-1969-abcp}, ενώ ένα κλασσικό εισαγωγικό κείμενο είναι
το \cite{de-bakker-1980-mtpc}. Ακολουθώντας αυτή την προσέγγιση, έχει
επίσης προταθεί η ανάπτυξη αποδείξεων ορθότητας παράλληλα με την
ανάπτυξη των προγραμμάτων \cite{dijkstra-1976-dp, gries-1981-sp}.
\end{itemize}

Θα πρέπει να σημειωθεί ότι αυτές οι τρεις κατηγορίες δεν πρέπει να
αντιμετωπίζονται ως αλληλοσυγκρουόμενες. Στην πραγματικότητα είναι
συμπληρωματικές και αλληλοεξαρτώμενες. Κάθε μια έχει τις εφαρμογές της
και εξυπηρετεί καλύτερα μια συγκεκριμένη κατηγορία εφαρμογών. Η
λειτουργική και η δηλωτική σημασιολογία μπορούν να χρησιμοποιηθούν για
τον ορισμό διερμηνέων για μια μελετώμενη γλώσσα, και κατά συνέπεια
βοηθούν στον ορισμό ή την αναμόρφωση μιας γλώσσας. Η αξιωματική
σημασιολογία είναι χρήσιμη για την απόδειξη ιδιοτήτων των προγραμμάτων.
Πιθανώς η κυριότερη εφαρμογή της τυπικής σημασιολογίας είναι η ταχεία
πρωτοτυποποίηση (rapid prototyping), με τη χρήση εργαλείων που
μεταφράζουν προδιαγραφές γλωσσών προγραμματισμού σε σωστούς
μεταγλωττιστές ή διερμηνείς.

Υπάρχουν φορμαλισμοί που έχουν επηρεασθεί και συνδυάζουν στοιχεία
περισσότερων από τις προαναφερθείσες κατηγορίες. Οι μηχανές αφηρημένης
κατάστασης (abstract state machines), γνωστές και ως εξελισσόμενες
άλγεβρες (evolving algebras) είναι ένας τέτοιος φορμαλισμός, που
διατυπώθηκε από τον Gurevich ως μια προσπάθεια γεφύρωσης του χάσματος
ανάμεσα σε τυπικά μοντέλα υπολογισμού και στις πρακτικές μεθόδους
προδιαγραφής \cite{gurevich-1992-eaads, gurevich-1995-ealg}. Η δραστική
σημασιολογία (action semantics), που αναπτύχθηκε από τους Mosses και
Watt, είναι ένα πρακτικό υπόβαθρο για την τυπική περιγραφή γλωσσών που
συνδυάζει χαρακτηριστικά και των τριών παραδοσιακών
προσεγγίσεων \cite{mosses-1992-as}.

Η δηλωτική σημασιολογία, ή η μαθηματική προσέγγιση στη σημασιολογία
γλωσσών προγραμματισμού, είναι ένας φορμαλισμός που διατυπώθηκε από
τους Scott και Strachey στα τέλη της δεκαετίας του 1960. Έκτοτε έχει
ευρέως μελετηθεί από διακεκριμένους ερευνητές και έχει χρησιμοποιηθεί
ως μέθοδος για τη σημασιολογική ανάλυση, την περιγραφή, την αξιολόγηση
αλλά και την υλοποίηση διαφόρων γλωσσών προγραμματισμού. Η θεμελιώδης
εργασία στη δηλωτική σημασιολογία είναι η \cite{scott-1971-tmscl}.
Άλλές εισαγωγικές εργασίες που περιλαμβάνουν χρήσιμη βιβλιογραφία είναι
οι \cite{tennent-1976-dspl} και \cite{mosses-1990-ds}. Εισαγωγικά
βιβλία που παρουσιάζουν σε μεγαλύτερο βάθος την σχετική θεωρία και τις
τεχνικές που έχουν αναπτυχθεί είναι τα \cite{milne-1976-tpls},
\cite{stoy-1977-dsssaplt}, \cite{gordon-1979-ddpl},
\cite{allison-1986-pids} και \cite{schmidt-1986-dsmld}. Ένα βιβλίο
μεταπτυχιακού επιπέδου με μεγαλύτερο μαθηματικό βάθος είναι
το \cite{gunter-1992-splst}. Η παρούσα διατριβή έχει επηρεασθεί σε
μεγάλο βαθμό από το \cite{tennent-1991-spl}, ένα εξαιτερικό βιβλίο που
αποκαλύπτει τη σύνδεση μεταξύ σύνταξης και διαφόρων πλευρών της
σημασιολογίας. Το ίδιο πραγματοποιείται από το
 \cite{mitchell-1996-fpl}, που εστιάζεται κυρίως στη μαθηματική
θεμελίωση των διαφόρων προσεγγίσεων. Τέλος, μια επισκόπηση του
ερευνητικού πεδίου δίνεται στο \cite{jung-1996-ddshaop}.

Σύμφωνα με τη δηλωτική προσέγγιση, η σημασιολογία των γλωσσών
προγραμματισμού περιγράφεται με την συσχέτιση μαθηματικών
\emph{ερμηνειών} (denotations) σε προγράμματα και τμήματα προγραμμάτων.
Οι ερμηνείες είναι συνήθως συναρτήσεις υψηλού βαθμού πάνω σε κατάλληλες
μαθηματικές οντότητες, όπως τα \emph{πεδία} (domains), η θεωρία των
οποίων συνοψίζεται στο κεφάλαιο~\ref{ch:mathematics}. Μια από τις βασικές
ιδιότητες της δηλωτικής σημασιολογίας είναι η \emph{συνθετικότητα}
(compositionality), δηλαδή το γεγονός ότι η ερμηνεία μιας πρότασης
μπορεί να υπολογισθεί με την κατάλληλη σύνθεση των ερμηνειών των
τμημάτων της πρότασης, όπως αυτά καθορίζονται από τη συντακτική δομή.
Παρότι οι ερευνητές δεν έχουν συμφωνήσει σε μια κοινά αποδεκτή
μεταγλώσσα για την παράσταση των ερμηνειών και ότι υπάρχει αρκετά
μεγάλη διαφοροποίηση στους συμβολισμούς που χρησιμοποιούνται από
διαφόρους συγγραφείς, φαίνεται ότι οι παραλλαγές του λογισμού-$\lambda$
($\lambda$-calculus) πάνω σε πεδία είναι πολύ δημοφιλείς. Αυτή η
προσέγγιση υιοθετείται στην παρούσα διατριβή.

Ένα από τα σημαντικότερα μειονεκτήματα της κλασσικής δηλωτικής
σημασιολογίας είναι η έλλειψη δόμησης (modularity). Μικρές αλλαγές ή
επεκτάσεις στον ορισμό μιας γλώσσας συνεπάγονται συχνά τεράστιες
αλλαγές στην τυπική της σημασιολογία. Κατά συνέπεια, παρότι η δηλωτική
σημασιολογία είναι ένας κατάλληλος και κομψός φορμαλισμός για γλώσσες
ως μεσαίου μεγέθους, δεν είναι εύκολη η χρήση της στην περίπτωση
πραγματικών γλωσσών προγραμματισμού.\footnote{Στην παρούσα διατριβή, ο
όρος ``πραγματικές γλώσσες προγραμματισμού'' σημαίνει γλώσσες
προγραμματισμού υψηλού επιπέδου που χρησιμοποιούνται ευρέως στην πράξη
για την ανάπτυξη λογισμικού, σε αντιδιαστολή με γλώσσες που
σχεδιάζονται και χρησιμοποιούνται σε ακαδημαϊκά εργαστήρια για
πειραματικούς σκοπούς. Φυσικά αυτό δε σημαίνει ότι οι πρώτες είναι
περισσότερο πραγματικές, ή καλύτερες από τις δεύτερες. Αρκετές φορές
συμβαίνει μάλλον το αντίθετο.} Επιπλέον, δεν είναι εύκολη η
επαναχρησιμοποίηση τμημάτων της περιγραφής δηλωτικής σημασιολογίας μιας
γλώσσας προγραμματισμού για την περιγραφή μιας άλλης γλώσσας. Η μελέτη
μεμονωμένων χαρακτηριστικών των γλωσσών προγραμματισμού είναι
ευκολότερη και κατά συνέπεια επιθυμητή. Όμως, αυτό προϋποθέτει ότι θα
είναι αργότερα δυνατό να ενωθούν τα κομμάτια και να δημιουργηθεί μια
πλήρης δηλωτική περιγραφή για ολόκληρη τη γλώσσα προγραμματισμού. Αυτό
το βήμα σύνθεσης είναι το σημείο αποτυχίας της κλασσικής δηλωτικής
σημασιολογίας.

Η χρήση της \emph{θεωρίας κατηγοριών} (category theory) και των
\emph{μονάδων} (monads) έχει προταθεί ως λύση στο πρόβλημα της έλλειψης
δόμησης και είναι αρκετά δημοφιλής στην κοινότητα των ερευνητών της
δηλωτικής σημασιολογίας. Όπως προτάθηκε από τον Moggi, η διαισθητική
αιτιολόγηση της χρήσης των μονάδων στη δηλωτική σημασιολογία είναι ότι
οι υπολογισμοί με αποτέλεσμα μια τιμή ενός πεδίου $V$ μπορούν να
αναπαρασταθούν ως στοιχεία ενός πεδίου $M(V)$, όπου $M$ είναι μια
κατάλληλη μονάδα \cite{moggi-1989-clcm}. Τα χαρακτηριστικά των γλωσσών
προγραμματισμού μπορούν να μελετηθούν ανεξάρτητα το ένα από το άλλο, με
την επιλογή σχετικά απλών μονάδων για την αναπαράστασή του, και
αργότερα να συνδυασθούν σε μια πλήρη σημασιολογική περιγραφή για τη
γλώσσα. Επίσης, οι μονάδες έχουν πρόσφατα προταθεί ως ένας κομψός
τρόπος για την εισαγωγή προστακτικών χαρακτηριστικών στο συναρτησιακό
μοντέλο προγραμματισμού, και πολλές συναρτησιακές γλώσσες τις
υποστηρίζουν άμεσα.

Στη διατριβή αυτή γίνεται χρήση της τεχνικής των μονάδων και ως
αποτέλεσμα αυτής καταδεικνύεται ότι η σημασιολογία βελτιώνεται
σημαντικά ως προς την δόμηση και την κομψότητα. Μια σύντομη εισαγωγή
στις μονάδες, ο ακριβής συμβολισμός που χρησιμοποιείται σε αυτή τη
διατριβή και αναφορές σε χρήσιμη βιβλιογραφία δίνονται στο
κεφάλαιο~\ref{ch:mathematics}. Για αναλυτικές εισαγωγές στις μονάδες
και τη χρήση τους στη δηλωτική σημασιολογία, ο αναγνώστης παραπέμπεται
στα \cite{moggi-1990-avpl} και \cite{wadler-1992-efp}.


\section{Επισκόπηση της διατριβής%
  \label{sec:intro:overview}}

Το κύριο αντικείμενο αυτής της διατριβής είναι η ανάπτυξη και
αξιολόγηση μιας τυπικής περιγραφής της σημασιολογίας της γλώσσας
προγραμματισμού C. Η προτεινόμενη σημασιολογία πρέπει να πληρεί τις
παρακάτω απαιτήσεις:
\begin{itemize}
%
\item \emph{Ορθότητα}: η τυπική περιγραφή πρέπει να αποδίδει όσο το
δυνατόν πιο πιστά την άτυπη σημασιολογία της ANSI~C, όπως αυτή
περιγράφεται στο πρότυπο. Οι περισσότερες τυπικές περιγραφές της
σημασιολογίας πραγματικών γλωσσών προγραμματισμού που έχουν προταθεί
στη βιβλιογραφία είναι ανακριβείς, σε κάποιο βαθμό, είτε λόγω
ηθελημένων απλοποιήσεων είτε κατά λάθος. Λαμβάνοντας υπόψη την
πολυπλοκότητα των γλωσσών αυτών, πρέπει κανείς να παραδεχθεί ότι μια
ανακριβής σημασιολογία είναι εντούτοις χρήσιμη, υπό την προϋπόθεση οι
ανακρίβειες να είναι σαφώς καταγεγραμμένες.
%
\item \emph{Πληρότητα}: η γλώσσα που περιγράφεται πρέπει να είναι όσο
το δυνατό μεγαλύτερο υποσύνολο της ANSI~C. Στην περιγραφή της τυπικής
σημασιολογίας μιας πραγματικής γλώσσας προγραμματισμού, είναι συχνή η
παράλειψη πολύπλοκων χαρακτηριστικών της γλώσσας, που δεν μπορούν να
περιγραφούν με απλό και κομψό τρόπο. Είναι επίσης συχνή η αντιμετώπιση
ορισμένων χαρακτηριστικών ως συντακτικών κατασκευασμάτων που μπορούν να
ορισθούν βάσει άλλων χαρακτηριστικών (syntactic sugar). Η πρώτη τακτική
οδηγεί σε ανακριβείς τυπικές περιγραφές και πρέπει να αποφεύγεται, όσο
αυτό είναι δυνατό. Η δεύτερη τακτική, παρότι δεν επηρεάζει την ορθότητα
της σημασιολογίας, αποφεύγεται επίσης στην παρούσα διατριβή, καθώς
συχνά στερεί τη σημασιολογική περιγραφή από την άμεση σύνδεσή της με τη
σύνταξη της γλώσσας.
%
\item \emph{Απλότητα}: η τυπική περιγραφή πρέπει να διατηρείται όσο το
δυνατόν απλούτερη. Το σκεπτικό πίσω από αυτή την απαίτηση είναι ότι τα
απλά τυπικά συστήματα είναι ευκολότερα στην ανάπτυξη, κατανόηση,
γενικότερα διαχείριση, αλλά και (κυρίως) στη χρήση. Η απαίτηση αυτή
έρχεται σε άμεση αντιπαράθεση με τις προηγούμενες δυο.
\end{itemize}
Οι δυο πρώτες απαιτήσεις θεωρούνται οι σημαντικότερες στο πλαίσιο αυτής
της διδακτορικής διατριβής. Επομένως, η προτεινόμενη σημασιολογία
πρέπει να είναι όσο το δυνατόν ορθότερη και πληρέστερη, σε σχέση με το
πρότυπο. Η απλότητα θα πρέπει να επιδιώκεται, όσο αυτό δεν επηρεάζει
τις άλλες δυο απαιτήσεις.


%%%  Bibliography

\bibliographystyle{softlab-thesis}
\bibliography{test}


%%%  Appendices

\backmatter

\appendix

\chapter{Ευρετήριο συμβολισμών}

$A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$.


%%%  End of document

\end{document}