Some Intentionally Provocative Remarks [Romanian]

Original in English by J Strother Moore

Câteva remarci provocatoare în mod intenţionat

Comparativ cu celelalte “cele mai bune idei” ce eu deja am menţionat, aceasta este foarte banală, dar cred că are o valoare practică importană pentru persoanele care doresc să proiecteze ad-hoc limbaje de programare şi doresc să verifice aplicaţiile scrise în aceste limbi. Şi o consecinţă a acestei idei este destul de puţin surprinzătoare pentru mine:

Dacă ar fi existat dezvoltatori decenţi de teoreme în 1960, Floyd şi Hoare nu ar inventa niciodată semantica lui Floyd-Hoare!

Mai jos, eu expun un punct de vedere personal al istoriei noastre CS, pe care o susţinem.

Semanticile operaţionale erau înţelese înainte de semantica lui Floyd-Hoare. De exemplu, în 1962, în seminalul său “Către o ştiinţă matematică de calcul,” McCarthy a scris “sensul unui program este definit prin efectul său asupra vectorului de stare”.

Semanticii operaţionale au unele puncte puternice semantica lui Floyd-Hoare nu are.

În contrast cu semantica lui Floyd-Hoare, semantica operaţională are următoarele proprietăţi:

  • Acestea pot fi formalizate într-un cadru matematic clasic, de exemplu, logica de primul ordin cu inducţie, dar nu un amestec de logică şi sintaxa limbajului de programare. În special, ele nu necesită noi reguli de inferenţă dincolo de cele studiate de către logicieni sute de ani.

  • Se pot folosi tehnici tradiţionale matematice, nu numai pentru a demonstra corectitudinea totală şi parţială a unor programe specifice, ci pentru a demonstra proprietăţi ale limbajului de programare în sine, şi pentru a se referă la diferite limbi.

  • Se pot scrie modele operaţionale semantice, astfel încât acestea sunt direct executabile şi pot fi astfel utilizate ca interpreţi pentru limbajul de programare dat.

  • Este în general simplu de a compara un model operaţional semantic la o punere în aplicare a limbii, deoarece ambele sunt descrise în termeni de operaţii pe valorile de date ale limbii.

Cu toate acestea, semantica lui Floyd-Hoare are o proprietate minunată: dovezi de cod prin metoda de afirmaţie inductivă sunt relativ simple. Aceasta se datorează faptului că toate obligaţiile dovezilor se adresează direct proprietăţi ale codului de utilizator şi toate problemele lingvistice sunt scoase din ele.

Dar, în măsura în care pot spune, nimeni nu ştia cum să realizeze o afirmaţie standartă în stilul probei inductive direct în semanticile operaţionale. “Ideea cea mai bună” ce eu am descris mai jos arată cum să faci asta! Este într-adevăr banal şi necesită doar o mecanizare bună a demonstratorului de teoreme.

Stilul afirmării inductive – unde se produce adnotarea textului programului, cu afirmaţii care se presupun să fie adevarate de fiecare dată când sunt întâlnite în timpul execuţiei – ne întoarcem la Goldstine şi von Neumann (1946) şi Turing (1949). Aceste aplicaţii iniţiale ale metodei au fost informale, în sensul că nici un proces formal definit nu a fost dat pentru a genera formule pentru a dovedi. În schimb, practicanţii timpurii tocmai au avansat cu dovezile lor. Esenţa consta nu în formalitate, ci în precizie matematică obişnuită şi argument.

Dar toate prezentările formale ale metodei descriu în esenţă un proces meta-logic de transformare, de multe ori numit verificare, condiţie, generare (VCG), care este o regulă de inferenţă ce permite dovedirea afirmaţiilor din alte afirmaţii şi textul programului intervenit. Din punct de vedere tehnic, regula VCG este o regulă derivată care poate fi dovedită a fi valabil dintr-o descriere semantică operaţională a limbajului de programare. Atât Floyd, cît şi Hoare au fost destul de expliciţi la cea ce ţine de utilizarea semanticii operaţionale pentru a justifica valabilitatea tehnicilor lor. Bănuiesc că fiecare familiarizat cu lucrările lor seminale ar recunoaşte ideea de aici, doar ca aplicarea a argumentelor lor stabile, la un program de adnotare dat. Deci, ideea mea nu este cu adevarat nouă. Dar ea tot mai mult miră, luînd în vedere faptul că nimeni nu a folosit-o!

Logica de programare au fost introdusă pentru a face procesul de VCG primitiv, cu privire la sistemul formal şi pentru a unifica programare şi dovada.

Cu toate acestea, atunci când totul a fost spus şi făcut, punerea în aplicare a logicii de programare, în general, a constat din două părţi. Prima parte este VCG şi a doua parte este un demonstrator de teoreme pentru condiţiile de verificare (VC-uri).

Dar definind semantici pentru un limbaj de programare modern, cum ar fi Java, este greu (de exemplu, predispus la erori), pentru că atât de mult se întâmplă în construcţii lingvistice tipice, cum ar fi invocarea metodei, construirea unui nou obiect, sau scrierea la un câmp într-un obiect. Şi semantica lui Hoare impune ca proiectantul să descrie toate acestea, la meta nivel: ca o formulă de transformare, mai degrabă decât ca un de transformare de date (sau de stare). Pentru a face procesul de scriere a VCG chiar mai predispus la eroare, este des acceptat faptul că unele teoreme de demonstrare trebuie să se facă “în zbor”, cînd formule sunt generate, deoarece în caz contrar, numărul şi dimensiunea de VC-uri creşte excesiv.

Astfel, pentru a utiliza un o logică de programare mecanizată, în general, trebuie de avut încredere în două instrumente foarte mari şi complicate: un VCG şi un demonstrator de teoreme.

Dar este banal de a utiliza metoda de afirmare inductivă într-un cadru semantic operaţional. Este nevoie de doar un demonstrator de teoreme decent pentru a face simbolul ca să lucreze. Dacă exprimaţi problema în mod “corect”, atunci puteţi obţine un demonstrator de teoreme pentru a genera condiţii simplificate de verificare în zbor. Şi astfel, trebuie doar să că încredeţi doar unui instrument: demonstrator de teoreme.

Dacă am fi avut demonstratori decenţi de teoreme la începutul anilor 1960, eu cred că acest fapt ar fi fost la fel de evident cum aceasta este acum şi niciodată nu ar fi fost necesar de a inventa logica de programare.

Sfat

De ce intrăm într-o mlaştină, atunci când există un drum curat în jurul ei?

Astăzi, o mulţime de oameni proiectează limbaje de programare, de exemplu, microcoduri de motoare pentru dispozitive cu destinaţie specială. Acestea sunt adesea critice pentru siguranţă şi nu există interes clar în verificarea programelor care urmează să fie scrise. Astfel de implementatori lingvistici ar putea fi tentaţi să oficializeze limba lor nouă prin scrierea de VCG. Dar nu! Este o activitate predispusă la eroare. Ar trebui oricum să aveţi un demonstrator de teoreme de încredere. Deci, de ce nu scrieţi semantica dvs. în mod operaţional şi nu succesaţi cu dovezi inductive a stilului de afirmare?

Ideea de bază

Deci, imaginati-va că aveţi semantici operaţionale acordate de un singur pas a funcţiei “starea următoare”. Să numim aceasta pasul funcţiei. Îmi imaginez că programul va fi executat, împreună cu contor de program, PC-ul, care este parte a stării. Semantica limbii este dat prin pas aplicat iterativ la starea iniţială.

Acum, să presupunem mai departe că aveţi o adnotare a programului ce asociază afirmaţiile cu PC-uri specifice. Pentru a face ca procesul să lucreze, ar trebui să reducem “fiecare bucla” cu o afirmaţie, şi anume, să ne asigurăm că codul nu se poate executa nimic tot timpul, fără a se confruntă cu o afirmaţie. Într-un program simplu, cu o buclă, se adnotează, în general, intrarea PC-ului, cu o afirmaţie numită pre-condiţie, partea de sus a buclei, cu o buclă invariantă, şi de ieşire, numită post-condiţie. Vreţi să demonstraţi dacă o pre-condiţie se deţine la intrarea şi executarea ajunge la ieşire, apoi post-condiţie se deţine.

Problema cu dovedirea acestui lucru este că va trebui de a executa (simbolic) un număr arbitrar de paşi pentru a obţine de la o afirmaţie la alta, pentru a ştie ce să dovedească.

Cu acest mod, există şi un alt obieciv, de a completa afirmaţiile, astfel că ei să reprezinte un pas invariant înţelept. Pentru a le finaliza, definim doar un predicat, inv, care ia starea şi nu o fracţiune de caz de ceea ce este PC-ul. În cazul în care PC-ul este unul dintre cei adnotaţi, Inv verifică doar afirmaţia corespunzătoare. În cazul în care PC-ul nu este unul dintre cei adnotaţi, invarianta (s) este definită a fi invarianta (pasul (s)).

Dacă încercaţi să dovediţi faptul că Inv (s) implică Inv (pas (s)) – aşa este, dacă încercaţi să dovediţi faptul că este Inv este invarianta în conformitate cu pas – veţi genera doar condiţiile standarte de verificare ca subobiective!

Pentru a afla mai multe, citiţi cartea!

Referinte

  • Inductive Assertions and Operational Semantics, CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 289-303, 2003.
  • Inductive Assertion Style Proofs via Operational Semantics — A talk given at IFIP WG2.2, Udine, Italy, Sep 13, 2006. This talk is clearer, I think, than the one I gave at CHARME.
  • ACL2 demo session log – this is the session log of the demonstration I gave. The log has two parts. First I just prove a classic Boyer-Moore theorem — the associativity of append — to remind the audience of the theorem prover's basic style. Second, I show a complex operational semantics for the JVM, as described in the talk and use it to verify the partial correctness of a simple program that computes half of an even natural (and runs forever on odd naturals).
  • Java session log – shows the trivial program we will verify. To see the JVM model compute on these same examples and then see the partial correctness proof, see the second half of the ACL2 demo session log above.

ok ok