Кіріспе

ACL2 (A Computational Logic for Applicative Common Lisp) – бағдарламалау тілі, бірінші реттік логикадағы кеңейтілетін теориясы және автоматтандырылған теореманы дәлелдейтін жүйеден тұратын бағдарламалық кешен. ACL2 негізінен бағдарламалық және аппараттық құралдарды тексеру үшін индуктивті логикалық теорияларда автоматты қорытынды шығаруды қолдауға арналған. ACL2 кіріс тілі мен іске асыру Common Lisp тілінде жазылған. ACL2 – тегін және ашық кодты бағдарламалық қамтамасыз ету.

Шолу

ACL2 бағдарламалау тілі Common Lisp-тің қолданбалы (қосымша әсерлерсіз) түрі болып табылады. ACL2 типтелмеген. Барлық ACL2 функциялары толық – яғни, әрбір функция ACL2 әлемінің әрбір нысанын өзінің әлеміндегі басқа нысанға бейнелейді. ACL2 негізгі теориясы оның бағдарламалау тілінің семантикасын және кіріктірілген функцияларын аксиоматизациялайды. Бағдарламалау тіліндегі пайдаланушы анықтамалары, егер олар анықтамалық принципті қанағаттандырса, теорияның логикалық дұрыстығын сақтай отырып, теорияны кеңейтеді. ACL2 теореманы дәлелдеушінің ядросы термин қайта жазуға негізделген, және бұл ядро кеңейтілуге жарамды, себебі пайдаланушылар ашқан теоремалар кейінгі болжамдар үшін қосымша дәлелдеу тәсілдері ретінде қолданылуы мүмкін. ACL2 – Бойер-Мур теоремасын дәлелдеушінің, NQTHM-нің «кәсіби деңгейдегі» нұсқасы. Осы мақсатқа жету үшін ACL2 қызықты математикалық және есептеу теорияларын жасаудағы таза инженерияны қолдайтын көптеген мүмкіндіктерге ие. ACL2 сонымен қатар Common Lisp-ке негізделгендіктен тиімділікке қол жеткізеді; мысалы, индуктивті тексерудің негізі болып табылатын бірдей сипаттама жинақталып, тікелей орындалуы мүмкін. 2005 жылы ACL2-ні қамтитын Бойер-Мур дәлелдеушілерінің авторлары ACM Software System Award сыйлығын «қауіпсіздікке қатысты аппараттық және бағдарламалық құралдарды тексеру үшін формалды әдіс құралы ретінде ең тиімді теореманы дәлелдеушіні ( ) дамытып, енгізгені үшін» алды.

Дәлелдендіру

ACL2 көптеген өнеркәсіптік қолданыстарға ие болды. 1995 жылы J Strother Moore, Matt Kaufmann және Tom Lynch ACL2 жүйесін пайдаланып, Pentium FDIV қатесінен кейін AMD K5 микропроцессорының қозғалмалы нүктелі бөлу операциясының дұрыстығын дәлелдеді. ACL2 құжаттамасының «Қызықты қолданыстар» бөлімінде жүйенің кейбір қолданыстарының қысқаша сипаттамасы келтірілген. ACL2-ні өнеркәсіптік тұрғыда пайдаланатындардың қатарында AMD, Arm, Centaur Technology, IBM, Intel, Oracle және Collins Aerospace компаниялары бар.