\documentclass[diploma]{softlab-thesis}


%%%
%%%  The document
%%%

\begin{document}

%%%  Title page

\frontmatter

%%% TODO change
\title{Σχεδίαση και Επέκταση ενός Συστήματος Αυτόματης Αξιολόγησης Προγραμματιστικών Ασκήσεων}
\author{Αντώνιος Αγγελάκης}
\date{Μάρτιος 2018}
%%% TODO change
\datedefense{17}{3}{2018}

\supervisor{Νικόλαος Παπασπύρου}
\supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}

%%% TODO change middle names?
\committeeone{Νικόλαος Παπασπύρου}
\committeeonepos{Αν. Καθηγητής Ε.Μ.Π.}
\committeetwo{Αριστείδης Παγουρτζής}
\committeetwopos{Αν. Καθηγητής Ε.Μ.Π.}
\committeethree{Γεώργιος Στάμου}
\committeethreepos{Αν. Καθηγητής Ε.Μ.Π.}

%%% TODO change
\TRnumber{CSD-SW-TR-42-18}  % number-year, ask nickie for the number
\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}

\maketitle


%%%  Abstract, in Greek

%%% TODO change
\begin{abstractgr}%
  Σκοπός της παρούσας εργασίας είναι αφενός η σχεδίαση μίας απλής
  γλώσσας υψηλού επιπέδου με υποστήριξη για προγραμματισμό με
  αποδείξεις, αφετέρου η υλοποίηση ενός μεταγλωττιστή για τη γλώσσα
  αυτή που θα παράγει κώδικα για μία γλώσσα ενδιάμεσου επιπέδου
  κατάλληλη για δημιουργία πιστοποιημένων εκτελέσιμων.

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

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

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

  Επιτύχαμε να διατηρήσουμε τη γλώσσα κοντά στο ύφος των ευρέως
  διαδεδομένων συναρτησιακών γλωσσών, καθώς και να διαχωρίσουμε τη
  φάση προγραμματισμού από τη φάση απόδειξης της ορθότητας των
  προγραμμάτων. Έτσι ένας μέσος προγραμματιστής μπορεί εύκολα να
  προγραμματίζει στη γλώσσα που προτείνουμε με τον τρόπο που ήδη
  γνωρίζει, και ένας γνώστης μαθηματικής λογικής να αποδεικνύει σε
  επόμενη φάση την μερική ορθότητα των προγραμμάτων. Ως απόδειξη της
  πρακτικότητας της προσέγγισης αυτής, παραθέτουμε ένα σύνολο
  παραδειγμάτων στη γλώσσα με απόδειξη μερικής ορθότητας.
%%% TODO change
\begin{keywordsgr}
Γλώσσες προγραμματισμού, Προγραμματισμός με αποδείξεις, Ασφαλείς γλώσσες
προγραμματισμού, Πιστοποιημένος κώδικας.
\end{keywordsgr}
\end{abstractgr}


%%%  Abstract, in English

%%% TODO change
\begin{abstracten}%
  The purpose of this diploma dissertation is on one hand the design
  of a simple high-level language that supports programming with
  proofs, and on the other hand the implementation of a compiler for
  this language. This compiler will produce code for an
  intermediate-level language suitable for creating certified
  binaries.

  The need for reliable and certifiably secure code is even more
  pressing today than it was in the past. In many cases, security and
  software compatibility issues put in danger the operation of large
  systems, with substantial financial consequences. The lack of a
  formal way of specifying and proving the correctness of programs that
  characterizes current programming languages is one of the main reasons
  why these issues exist. In order to address this problem, a number of
  frameworks with support for certified binaries have recently been
  proposed. These frameworks offer the possibility of specifying and
  providing a formal proof of the correctness of programs. Such a proof
  can easily be checked for validity before running the program.

  The frameworks that have been proposed are intermediate-level in
  nature, thus the process of programming in these is rather cumbersome.
  The high-level languages that accompany some of these frameworks,
  while very expressive, are hard to use. A simpler high-level language,
  like the one proposed in this dissertation, would enable further use
  of this programming idiom.

  In the language we propose, the programmer specifies the partial
  correctness of a program by annotating function definitions with pre-
  and post-conditions that must hold for their parameters and results.
  The programmer also provides a set of theorems, based on which proofs
  of the proper implementation and use of the functions are constructed.
  An implementation in OCaml of a compiler from this language to the
  NFLINT certified binaries framework was also completed as part of this
  dissertation.

  We managed to keep the language close to the feel of the current
  widespread functional languages, and also to fully separate the
  programming stage from the correctness-proving stage. Thus an average
  programmer can program in a familiar way in our language, and later an
  expert on formal logic can prove the semi-correctness of a program.
  As evidence of the practicality of our design, we provide a number of
  examples in our language with full semi-correctness proofs.
\begin{keywordsen}
Programming languages, Programming with proofs, Secure programming
languages, Certified code.
\end{keywordsen}
\end{abstracten}


%%%  Acknowledgements

%%% TODO change
\begin{acknowledgementsgr}
Ευχαριστώ θερμά τον επιβλέποντα καθηγητή αυτής της διατριβής,
κ.~Γιάννη Παπαδάκη, για τη συνεχή καθοδήγηση και εμπιστοσύνη
του. Ευχαριστώ επίσης τα μέλη της συμβουλευτικής επιτροπής,
κ.κ.~Νίκο Παπαδόπουλο και Γιώργο Νικολάου για την πρόθυμη και
πάντα αποτελεσματική βοήθειά τους, τις πολύτιμες συμβουλές και
τις χρήσιμες συζητήσεις που είχαμε.  Θέλω να ευχαριστήσω ακόμα
τον συμφοιτητή και φίλο Πέτρο Πετρόπουλο, ο οποίος με βοήθησε σε
διάφορα στάδια αυτής της εργασίας.  Θα ήθελα τέλος να ευχαριστήσω
την οικογένειά μου και κυρίως τους γονείς μου, οι οποίοι με
υποστήριξαν και έκαναν δυνατή την απερίσπαστη ενασχόλησή μου τόσο
με την εκπόνηση της διπλωματικής μου, όσο και συνολικά με τις
σπουδές μου.
\end{acknowledgementsgr}


%%%  Various tables

\tableofcontents
\listoftables
\listoffigures


%%%  Main part of the book

\mainmatter

\chapter{Εισαγωγή}

\section{Σκοπός}

Ο σκοπός της παρούσας διπλωματικής εργασίας είναι ο σχεδιασμός 
και η υλοποίηση νέων δυνατοτήτων σε ένα σύστημα αυτόματης αξιολόγησης
προγραμματιστικών ασκήσεων. Το σύστημα που τροποποιήθηκε, όπως θα περιγραφεί
παρακάτω, χρησιμοποιείται τόσο από το Εργαστήριο Τεχνολογίας Λογισμικού (ΤODO links edw??)
όσο και από την Ελληνική Εταιρεία Επιστημόνων και Επαγγελματιών Πληροφορικής
και Επικοινωνιών (ΕΠΥ) για τη διοργάνωση των Πανελλήνιων Διαγωνισμών Πληροφορικής.

\bigskip

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

\bigskip

Ο grader, στην πρότερη κατάσταση του, επέτρεπε μόνο τη δημιουργία
μεμονωμένων αρχείων ελέγχου και όχι συνδυαστικών ομάδων καθιστώντας
δύσκολη τη δημιουργία προβλημάτων με δυαδικά αποτελέσματα, π.χ. σωστό/λάθος.
Επιπροσθέτως, δεν υπήρχε η επιλογή για προσθήκη αρχείων ελέγχου αξιολόγησης
χωρίς επιρροή στην αρχική αξιολόγηση μιας υποβολής ως θετική ή αρνητική.

\bigskip

Η αρχική σχεδίαση του grader είχε σκοπό τη δημιουργία ενός συστήματος αυτόματης
αξιολόγησης για διαγωνισμούς πληροφορικής, για να χρησιμοποιηθεί κυρίως από την
ΕΠΥ. Ως αποτέλεσμα, κάθε πρόβλημα αντιστοιχίζεται σε έναν μόνο διαγωνισμό και τόσο
οι διαγωνιζόμενοι όσο και οι υποβολές τους συνδέονται με το πρόβλημα. Για τη χρήση
του grader σε εργασίες προγραμματισμού, θα μας ήταν προτιμότερο να υπάρχει 
διαχωρισμός προβλήματος και υποβολών ώστε τα προβλήματα να μπορούν να 
επαναχρησιμοποιηθούν ευκολότερα.

\bigskip

Επιπλέον, κρίθηκε σημαντικό να προστεθεί η Python στις διαθέσιμες γλώσσες υποβολής
καθώς πρόκειται για μια από τις πλέον δημοφιλείς γλώσσες και χρησιμοποιείται ως
εισαγωγική γλώσσα προγραμματισμού σε σημαντικά ακαδημαϊκά ιδρύματα, όπως είναι το 
MIT και το Stanford (TODO citation needed). Τέλος, ήταν απαραίτητο να γίνουν μικρές
βελτιστοποιήσεις στη λογική του grader, να προστεθούν μικρότερες δυνατότητες που
επιδιώκουν τη βελτίωση της ευκολίας χρήσης για διαγωνιζόμενους και διαχειριστές και
να αντικατασταθούν απαρχαιωμένα (TODO obsolete, pws na to pw) εργαλεία/βιβλιοθήκες
για την επίτευξη καλύτερης απόδοσης και ασφάλειας.

\bigskip

(TODO μηπως αλλη μια summary παραγραφο εδω;;)

\section{Δομή Εργασίας}

Η εργασία ακολουθεί την παρακάτω δομή:

\begin{itemize}
  \item Κεφάλαιο 2 \\
    σδασδκακξσδαδσα ακσξδκασξδακδσκξδ αξσδκξασκξδσακξδξκ ασδ
    ασξδκασκξδκσαξδ ασκξδκξασ δκασξδ ακσξδ ακσξδκαξσδ 
  \item Κεφάλαιο 3
\end{itemize}

\chapter{Συστήματα Αυτόματης Αξιολόγησης}

\chapter{Υπάρχον Σύστημα}

\chapter{Προσθήκη Ομάδων Αρχείων Ελέγχου}

\chapter{Σχεδίαση για διαχωρισμό Προβλημάτων - Διαγωνισμών}

\chapter{Λοιπές Προσθήκες}

\section{Προσθήκη γλώσσας προγραμματισμού Python}

\section{Προσθήκη blue tag για μη απαραίτητα αρχεία ελέγχου}

\chapter{Συμπεράσματα}

\section{Καταληκτικές Παρατηρήσεις}

\section{Μελλοντική Έρευνα}

%%%  Bibliography

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


%%%  Appendices

\backmatter

\appendix

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

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

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

%%% TODO change
\textbf{Haskell} : η γλώσσα της ζωής μου.

\chapter{Ευρετήριο αριθμών}

%%% TODO change
42 : life, the universe and everything.


%%%  End of document

\end{document}