Patikrintas kompiliavimas ir jo pasitikėjimo riba
Tyrimų kontekstas
research method · established · Patikros data 2026-10-10
Pagrindinė CompCert semantikos išsaugojimo teorema susieja priimtą C abstrakčiąją sintaksę su sugeneruota asemblerio abstrakčiąja sintakse: esant teoremos prielaidoms, sugeneruota elgsena patikslina leidžiamą pradinės programos elgseną.
Esminės žinios
Pagrindinė CompCert semantikos išsaugojimo teorema susieja priimtą C abstrakčiąją sintaksę su sugeneruota asemblerio abstrakčiąja sintakse: esant teoremos prielaidoms, sugeneruota elgsena patikslina leidžiamą pradinės programos elgseną. Ši teorema nepaverčia pradinės programos neapibrėžtos elgsenos saugia. Sintaksės analizė ir pirminis apdorojimas, asemblerio vertimas ir susiejimas, vykdymo bibliotekos, aparatinė įranga ir pasitikėjimas įrodymų tikrintuvu turi atskiras ribas; kompiliatoriaus bandymas su pavyzdžiu nėra įrodymas kiekvienai įvesčiai.
Sąlygos ir taikymo ribos
- Naudokite konkrečios teoremos formalius kalbos ir tikslinės sistemos modelius bei sėkmingo kompiliavimo prielaidas.
- Paskelbtas įrodymas ir teiginys buvo peržiūrėti; šiame įraše neteigiama, kad iš naujo pakartotinai atlikta įrodymo patikra ar patikrinta visa diegimo grandinė.
Šaltiniai · 2
Šaltiniai
Šaltiniai išlaiko savo taikymo ribas. Vien nuoroda nepatvirtina kiekvieno teiginio patikrinimo.
Pagrindimas ir peržiūra
Autorius patikrino šį anglišką teiginį, pateiktą lygtį, jei ji yra, ir nurodytas prielaidas pagal šias šaltinių vietas: §1.2: leidžiamos elgsenos išsaugojimas; C AST ir asemblerio AST ryšys bei kompiliavimo grandinės ribos; transf_c_program_correct ir atskiro kompiliavimo teoremos apibrėžimai. Patikra apsiriboja užrašytais teiginiais; neteigiama, kad visiškai atkurtas įrodymas, pakartotinai atlikta programinė įrodymo patikra ar aprėpta visa literatūra.
2026-10-10 · Autoriaus atlikta šaltinio teksto, teiginio, lygties ir taikymo srities patikra; grafo sąsajų aprėptis nurodyta atskirai. Prieš užbaigiant šaką būtina atskira nepriklausoma turinio, šaltinių ir inventoriaus peržiūra.
Įrašo informacija
Nuolatinė nuoroda į šį įrašą ↗- Įrašo identifikatorius
- research-info-compiler-semantic-preservation
- Versija
- research.1
- Struktūruotas žinyno įrašas
- Podiplominis ir tyrimų žinynas