On logical methods for specifications: abstract and type-theoretic approaches

Abstract

This thesis delves into the multifaceted role of specifications in formal methods, focusing on various theoretical and applied approaches to enhance the expressibility and applicability of software verification techniques, as well as on the implications that these methods have in the foundations of mathematics. It is structured into four parts, each hopefully contributing in its own manner to bridging the gap between abstract (mathematical or not) reasoning and practical software engineering tools. Part I examines specifications from a philosophical/methodological standpoint. It introduces a novel logical framework that describes how specifications influence software creation, adapted from a similar framework for scientific theorising. This part underscores the objective constraints specifications impose on programmers and discusses how translatability between outputs of different software creation processes might be (abstractly) expressed. Part II shifts focus to a practical application: it presents a software tool for converting (a subset of) Business Process Model and Notation (BPMN) diagrams into systems of the Privacy Calculus, a formalism developed for privacy compliance. This part showcases the implementation of formal methods in real-world scenarios, emphasising the importance of tool support in applying theoretical concepts to everyday practice. In Part III, the thesis explores the extension of Temporal Type Theory (TTT) with calendric types, integrating the basics concepts of the Calendar and Time Type System (CaTTS). This part demonstrates how advanced type theories can be adapted to handle practical concerns in software processes, such as the specification of time constraints. As an instance of such a practical concern, this part concludes with an exploration of how some temporal properties of business processes pertaining to (smart) contracts can be rigorously expressed in TTT extended with calendric types. Finally, Part IV shifts to the formalization of mathematics, specifically focusing on Homotopy Type Theory (HoTT) and its implementation in the UniMath library. This part contains a small demonstration of the potential of HoTT as a computational foundational framework for mathematics, showing how the algebraic notion of pre-bilattices, along with one of the most central theorems regarding it, can be defined in UniMath.

Η παρούσα διδακτορική διατριβή εξετάζει τον πολυδιάστατο ρόλο των προδιαγραφών στις τυπικές μεθόδους, εστιάζοντας σε διάφορες θεωρητικές και εφαρμοσμένες προσεγγίσεις για την ενίσχυση της εκφραστικότητας και της εφαρμοσιμότητας των τεχνικών επαλήθευσης της ορθότητας λογισμικού, καθώς και στις επιπτώσεις που έχουν αυτές οι μέθοδοι στα θεμέλια των μαθηματικών. Η διατριβή αποτελείται από τέσσερα μέρη, καθένα από τα οποία επιδιώκει να συμβάλει με τον δικό του τρόπο στη γεφύρωση του χάσματος μεταξύ της αφηρημένης (μαθηματικής ή μη) σκέψης και των εργαλείων που χρησιμοποιούνται στη μηχανίκευση λογισμικού. Το μέρος I εξετάζει τις προδιαγραφές από φιλοσοφική/μεθοδολογική άποψη. Εισάγει ένα νέο λογικό πλαίσιο που περιγράφει πώς οι προδιαγραφές επηρεάζουν τη δημιουργία λογισμικού, το οποίο αποτελεί παραλλαγή ενός παρόμοιου πλαισίου για τη δημιουργία επιστημονικών θεωριών. Αυτό το μέρος τονίζει τους αντικειμενικούς περιορισμούς που επιβάλλουν οι προδιαγραφές στους προγραμματιστές και εξετάζει πώς μπορεί να εκφραστεί (αφηρημένα) η μεταφρασιμότητα μεταξύ των αποτελεσμάτων διαφορετικών διαδικασιών δημιουργίας λογισμικού. Το μέρος II αφορά μια πρακτική εφαρμογή: παρουσιάζει ένα εργαλείο λογισμικού για τη μετατροπή (ενός υποσυνόλου) των διαγραμμάτων του προτύπου Business Process Model and Notation (BPMN) σε συστήματα του Λογισμού Ιδιωτικότητας, ο οποίος αποτελεί μια τυπική γλώσσα που έχει αναπτυχθεί για τον έλεγχο συμμόρφωσης σε πρωτόκολλα ιδιωτικότητας. Αυτό το μέρος αναδεικνύει την πρακτική εφαρμογή των τυπικών μεθόδων, δίνοντας έμφαση στη σημαντικότητα ύπαρξης εργαλείων που υποβοηθούν την εφαρμογή θεωρητικών κατασκευών στην πράξη. Στο μέρος III, εξετάζεται η επέκταση της Χρονικής Θεωρίας Τύπων (TTT) με ημερολογιακούς τύπους, ενσωματώνοντας τις βασικές έννοιες του συστήματος Calendar and Time Type System (CaTTS). Το εν λόγω μέρος δείχνει πώς οι προηγμένες θεωρίες τύπων μπορούν να προσαρμοστούν για να χειρίζονται πρακτικά ζητήματα σχετικά με το λογισμικό, όπως οι προδιαγραφές που αφορούν χρονικούς περιορισμούς. Ως παράδειγμα τέτοιου πρακτικού ζητήματος, το μέρος αυτό συμπεριλαμβάνει μία διερεύνηση του πώς ορισμένες χρονικές ιδιότητες υπηρεσιακών διεργασιών που σχετίζονται με (έξυπνα) συμβολαία μπορούν να εκφραστούν με τυπικό τρόπο στην επεκτεταμένη με ημερολογιακούς τύπους TTT. Τέλος, το μέρος IV μετατοπίζει τη συζήτηση στην τυποποίηση των μαθηματικών, δίνοντας έμφαση στην Ομοτοπική Θεωρία Τύπων (HoTT) και την υλοποίησή της στη βιβλιοθήκη UniMath. Αυτό το μέρος περιέχει μια μικρή επίδειξη της δυνατότητας της HoTT να αποτελέσει ένα υπολογιστικό θεμέλιο των μαθηματικών, δείχνοντας πώς η αλγεβρική έννοια των προ-διπλεγμάτων (pre-bilattices), μαζί με ένα από τα πιο κεντρικά θεωρήματα που την αφορούν, μπορούν να οριστούν στη βιβλιοθήκη UniMath.