isabelle — συγκεντρωτικός οδηγός — DedSec Project

Isabelle/HOL

Τι προσφέρει η γλώσσα

Η Isabelle είναι proof assistant. Οι προτάσεις ελέγχονται σε λογικό πλαίσιο, όχι μόνο με παραδείγματα εισόδων.

Μικρό παράδειγμα προς μελέτη

lemma add_zero: "n + (0::nat) = n"
  by simp

Εξήγησε τη δήλωση τύπου nat, άλλαξε μια προϋπόθεση και έλεγξε αν το simp εξακολουθεί να αποδεικνύει την πρόταση.

Τι να επαληθεύσεις

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

Παγίδα ειδική για το θέμα

Αδυναμία απόδειξης δεν σημαίνει ότι η πρόταση είναι ψευδής· ξεχώρισε μη εύρεση απόδειξης από αντιπαράδειγμα.

Εργαστήριο εξάσκησης: Isabelle

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

Πλήρες αρχείο θεωρίας

Δημιούργησε Numbers.thy μέσα σε Isabelle session:

theory Numbers
  imports Main
begin

lemma right_zero: "n + (0::nat) = n"
  by simp

lemma left_zero: "(0::nat) + n = n"
  by simp

end

Άνοιξέ το με Isabelle/jEdit ή χρησιμοποίησε το σύστημα build της εγκατάστασης. Εξήγησε γιατί οι δύο ισότητες ισχύουν για κάθε φυσικό αριθμό. Η σημείωση (0::nat) καθορίζει τον τύπο και η τακτική simp αξιοποιεί γνωστά λήμματα απλοποίησης. Δεν είναι απλή εκτέλεση test.

Αντιπαράδειγμα και ανοιχτή υποχρέωση

Σε προσωρινό αντίγραφο, άλλαξε τον πρώτο στόχο σε n + (0::nat) = n + 1. Για n=0, η αριστερή πλευρά είναι 0 και η δεξιά 1, οπότε η πρόταση είναι ψευδής. Η by simp δεν πρέπει να ολοκληρώνει μία σωστή απόδειξη. Μην εισάγεις sorry ή αυθαίρετο αξίωμα για να κρύψεις την αποτυχία. Γενικά, η αποτυχία ενός αυτοματοποιημένου αποδεικτή δεν σημαίνει ότι μία πρόταση είναι ψευδής· στη συγκεκριμένη περίπτωση υπάρχει σαφές αντιπαράδειγμα.

Ξεχώρισε διαφορετικές αστοχίες

Αφαίρεσε by simp από έγκυρο αντίγραφο και παρακολούθησε την υποχρέωση που μένει ανοιχτή. Επανέφερε την απόδειξη. Έπειτα γράψε λάθος όνομα στο imports Main και διαχώρισε το σφάλμα φόρτωσης θεωρίας από το ατελές λήμμα. Τέλος, απόδειξε την αντιμεταθετικότητα (n::nat) + m = m + n με κατάλληλο λήμμα της βιβλιοθήκης.

Παραδοτέα: έκδοση Isabelle, αποδεκτό αρχείο θεωρίας, δύο αποδείξεις, ένα αντιπαράδειγμα και πραγματική κατάσταση απόδειξης ή σφάλμα. Χωρίς Isabelle δήλωσε μαθηματική ανάλυση, όχι μηχανική επαλήθευση.

Isabelle — Διαδρομή ουσιαστικής εξάσκησης

Πρακτικές εργασίες

1. Όρισε μικρή πρόταση και τις παραδοχές της.
2. Κατασκεύασε σύντομη απόδειξη με έμπιστους κανόνες συμπερασμού.
3. Αφαίρεσε μία παραδοχή και έλεγξε αν η απόδειξη ισχύει.

Ερωτήσεις ουσίας

• Ο στόχος είναι εκτελέσιμη τιμή ή ελεγμένη πρόταση;
• Ποια εργαλεία εκτελούν ή ελέγχουν το παράδειγμα και σε ποια έκδοση;
• Ποιο είναι το μικρότερο ελεγμένο πρόγραμμα; Ποιες είναι οι παρενέργειες;
• Πώς γίνεται διάκριση μεταξύ σφάλματος σύνταξης, λογικής και περιβάλλοντος;
• Πώς δοκιμάζονται άκυρα δεδομένα χωρίς βλάβη σε αρχεία ή σύστημα;