| Isabelle | |
|---|---|
| Tip de | Demonstrator de teoreme |
| Dezvoltator | Paulson |
| Scris in | Poly/ML ; Scala |
| Sistem de operare | GNU/Linux [1] , Microsoft Windows [1] și macOS [1] |
| Prima editie | 1 mai 1989 |
| Platformă hardware | multiplatformă |
| ultima versiune | Isabelle2021-1 (decembrie 2021 ) |
| Stat | activ |
| Licență | BSD |
| Site-ul web | isabelle.in.tum.de |
Isabelle este un instrument interactiv de demonstrare automată care utilizează logica de ordin superior . Este implementat în același stil ca unul dintre primele astfel de instrumente - LCF și, la fel ca LCF, a fost inițial scris în întregime în Standard ML [2] . Sistemul conține un nucleu logic compact, care poate fi acceptat ca adevărat fără dovezi suplimentare (deși acest lucru nu este necesar). Ca instrument general, implementează o metalogică ( teoria tipului slab ) care este utilizată pentru a implementa mai multe variante ale logicii obiectelor Isabelle, cum ar fi logica de ordinul întâi (FOL), logica de ordin superior (HOL) sau teoria seturilor Zermelo-Fraenkel. (ZFC). Cea mai des folosită variantă a logicii obiectelor este Isabelle / HOL, precum și dezvoltări destul de serioase în domeniul teoriei mulțimilor au fost realizate folosind Isabelle / ZF.
Principala metodă de implementare a demonstrației lui Isabelle este o variantă de rezoluție de ordin superior bazată pe un algoritm de unificare de ordin superior . Fiind un sistem interactiv, Isabelle include, de asemenea, instrumente puternice de raționament automat, cum ar fi un motor de rescriere a termenilor , un solutor de tabel analitic , soluții externe de fezabilitate pentru probleme din diverse teorii conectate printr-o interfață plug-in externă specializată Sledgehammer, precum și demonstrarea automată externă a teoremei. instrumente. , cum ar fi E și SPASS . Isabelle a fost folosită pentru a formaliza numeroase teoreme din matematică și informatică, cum ar fi teorema de completitudine a lui Gödel, dovada lui Gödel a independenței axiomei de alegere , teorema privind distribuția numerelor prime . Isabelle a fost, de asemenea, folosită pentru a dovedi corectitudinea formală a protocoalelor criptografice și proprietățile semanticii limbajelor de programare.
Multe dintre dovezile formale obținute folosind Isabelle sunt disponibile public și sunt stocate în Arhiva de dovezi formale , care conține (din 2019) cel puțin 500 de articole, inclusiv mai mult de 2 milioane de linii de cod [3] .
Distribuit gratuit sub licența BSD . Autor - Lawrence Paulson ( ing. Lawrence Paulson ), numele este dat în onoarea fiicei lui Gerard Huet [4] .
Sistemul vă permite să scrieți dovezi în două stiluri - procedural și declarativ . Stilul procedural al probei precizează succesiunea de aplicare a tacticilor și procedurilor de probă. Acest lucru corespunde stilului în care lucrează de obicei matematicienii obișnuiți, dar astfel de dovezi sunt de obicei destul de greu de înțeles, deoarece atunci când le citesc, rezultatul care este planificat să fie obținut ca urmare a unei astfel de dovezi nu este evident.
Demonstrațiile declarative implementate într-un limbaj special de dovezi încorporat - Isar - specifică procedurile matematice specifice care trebuie aplicate. Sunt mai ușor de citit și verificat de către oameni.
În versiunile recente ale lui Isabelle, stilul de probă procedurală a fost depreciat. Arhiva Probelor Formale recomandă, de asemenea, ca dovezile să fie prezentate în stil declarativ [5] .
Un exemplu de demonstrație declarativă a contrariului, scrisă în Isar (dovada confirmă iraționalitatea rădăcinii pătrate a lui doi):
teorema sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" demonstrație fie ?x = "sqrt (real 2)" presupunem "?x ∈ ℚ" apoi obținem mn :: nat unde sqrt_rat: "¦?x¦ = real m / real n" și cei mai mici_termeni: "coprime m n" prin (regula Rats_abs_nat_div_natE) de unde "real (m^2) = ?x^2 * real (n^2)" prin (auto simp add: power2_eq_square) de aici eq: "m^2 = 2 * n^2" folosind of_nat_eq_iff power2_eq_square prin fastforce , prin urmare, "2 dvd m^2" prin simp , prin urmare, "2 dvd m" prin simp au dovada "2 dvd n" - din ‹2 dvd m› obțineți k unde "m = 2 * k" .. cu eq au "2 * n^2 = 2^2 * k^2" prin simp deci "2 dvd n^2" prin simp astfel "2 dvd n" prin simp qed cu ‹2 dvd m › au „2 dvd gcd m n” de (regula gcd_greatest) cu cei mai mici_terms au „2 dvd 1” de simp , astfel False folosind odd_one de blast qed qed
Isabelle a fost folosită de multe ori pentru a implementa metode formale în specificarea, dezvoltarea și verificarea sistemelor software și hardware.
În 2009, dezvoltatorii proiectului L4.verified , care a fost implementat la centrul de cercetare australian NICTA , au oferit pentru prima dată o dovadă formală a corectitudinii funcționale a nucleului sistemului de operare de uz general, și anume microkernel-ul seL4 (o versiune integrată sigură a L4 capabilă să lucreze în timp real) [ 6] . Dovada a fost construită și verificată de Isabelle/HOL; conține peste 200 de mii de linii de script de verificare pentru a verifica 7500 de linii de cod C. Verificarea acoperă codul, proiectarea și implementarea[ specificați ] . Ca parte a dovezii, sa demonstrat că codul C implementează corect specificația formală a nucleului. Dovada a scos la iveală 144 de erori în codul C al nucleului seL4 timpuriu și aproximativ 150 de probleme fiecare în arhitectura și specificațiile nucleului în sine.
Pentru limbajul de programare Lightweight Java folosind Isabelle, a fost obținută o dovadă a siguranței de tip [7] .
O listă de proiecte de cercetare [8] care utilizează Isabelle este menținută de autorul sistemului Paulson.
Există o serie de sisteme automate de demonstrare a teoremelor similare ca capabilități cu Isabelle , inclusiv: