Πέντε νέα αποτελέσματα παρουσιάζονται στη θεωρία της δομικής διακυβέρνησης για συστήματα γνωστικής ροής εργασιών. Τρία εξ αυτών μηχανοποιήθηκαν στο Coq 8.19, αξιοποιώντας τη βιβλιοθήκη Interaction Trees με παραμετροποιημένη συνεπαγωγή, ενώ δύο αποδείχθηκαν θεωρητικά με τη χρήση σαφών αναγωγών.
Αποτελέσματα Μηχανοποιημένα στο Coq 8.19 για τη Δομική Διακυβέρνηση
Το Συνεπαγωγικό Κατηγόρημα Ασφάλειας (gov_safe) και η Εφαρμογή του
Το Συνεπαγωγικό Κατηγόρημα Ασφάλειας (gov_safe) αποτελεί μια συνεπαγωγική ιδιότητα που αποτυπώνει την ασφάλεια διακυβέρνησης για άπειρες συμπεριφορές προγραμμάτων. Ο δείκτης του αποδεικνύεται ψευδής για μη διακυβερνώμενες εισόδους/εξόδους (I/O) και αληθής για διακυβερνώμενες ερμηνείες, γεγονός που έχει μηχανοποιηθεί.
Το Θεώρημα Αναλλοίωτου της Διακυβέρνησης στον Μετα-αναδρομικό Πύργο
Το Θεώρημα Αναλλοίωτου της Διακυβέρνησης καθορίζει ότι η διακυβέρνηση είναι ομοιόμορφη σε όλο τον μετα-αναδρομικό πύργο: η διακυβέρνηση στο επίπεδο n+1 ανάγεται σε διακυβέρνηση στο επίπεδο n. Αυτό το αποτέλεσμα έχει επίσης μηχανοποιηθεί.
Το Θεώρημα Επάρκειας: Πρωτογενείς Λειτουργίες για Ευφυή Συστήματα
Το Θεώρημα Επάρκειας αποδεικνύει ότι τέσσερις ατομικές πρωτογενείς λειτουργίες (κώδικας, λογική, μνήμη, κλήση) είναι εκφραστικά πλήρεις για οποιοδήποτε διακριτό ευφυές σύστημα. Αυτό τυποποιείται ως συνθετικό κλείσιμο μιας κατηγορίας Kleisli και το εύρημα είναι μηχανοποιημένο.
Αποτελέσματα με Θεωρητικές Αποδείξεις
Η Εναλλασσόμενη Κανονική Μορφή και η Αποσύνθεση Μηχανών
Η Εναλλασσόμενη Κανονική Μορφή παρέχει μια κανονική αποσύνθεση οποιασδήποτε μηχανής σε εναλλασσόμενα επίπεδα κώδικα και επίδρασης, συνοδευόμενη από ένα συρρέον σύστημα επανεγγραφής. Η απόδειξη αυτή πραγματοποιήθηκε θεωρητικά.
Το Θεώρημα Αναγκαιότητας και η Σημασιολογική Κρίση
Το Θεώρημα Αναγκαιότητας αποδεικνύει, μέσω σαφούς αναγωγής στο θεώρημα του Rice, ότι ένα αρχιτεκτονικά αδιαφανές συστατικό, συγκεκριμένα η πρωτογενής λειτουργία λογικής, είναι μαθηματικά αναγκαίο για προβλήματα που απαιτούν σημασιολογική κρίση. Η απόδειξη αυτή έγινε επίσης θεωρητικά.
Σύνδεση του Αφηρημένου Μοντέλου με το Περιβάλλον Εκτέλεσης
Η Επαληθευμένη Προδιαγραφή Διερμηνέα BEAM και οι Έλεγχοι
Μια έκτη συνεισφορά συνδέει το αφηρημένο μοντέλο με το αναπτυγμένο περιβάλλον εκτέλεσης. Η Επαληθευμένη Προδιαγραφή Διερμηνέα τυποποιεί τη λογική εμπιστοσύνης, ικανότητας και αλυσίδας κατακερματισμού του χρόνου εκτέλεσης BEAM στο Coq. Στη συνέχεια, το εν λειτουργία σύστημα ελέγχεται έναντι αυτής της προδιαγραφής χρησιμοποιώντας δοκιμές βασισμένες σε ιδιότητες, με πάνω από 70.000 τυχαία παραγόμενες ακολουθίες εντολών και μηδενικές διαφωνίες.
Συνολικές Τεχνικές Λεπτομέρειες της Μηχανοποίησης
Η συνολική μηχανοποίηση περιλαμβάνει περίπου 12.000 γραμμές κώδικα, κατανεμημένες σε 36 ενότητες, με 454 θεωρήματα και μηδέν παραδεκτά λήμματα.
