1

Program: POS CCE- Axa 2- Domeniul 2.1 - Operațiunea 2.1.2 Denumire Proiect: Un cadru de lucru bazat pe Semantică Executabilă pentru Proiectarea Riguroasă, Analiza și Testarea Sistemelor - DAK ID / Cod SMIS:602/12516 Nr. Contract:161/15.06.2011

RAPORTUL FINAL (anexa)

1. Introducere Calculatoarele au devenit deja o parte integrantă a vieții noastre. În afară de creșterea utilizării calculatoarelor personale, dispozitivele electronice programabile au devenit prezente în toate aspectele moderne ale vieții, de la aparate electrocasnice, până la sisteme critice cum ar fi dispozitive folosite în industria transporturilor sau a dispozitivelor medicale. Mai mult decât atât, internetul și era informației au adus o gamă întreagă de servicii, aflate până de curând la distanță, la doar un clic depărtare. Toate aceste servicii, fie ele oferite prin sisteme încorporate sau prin calculatoare personale sau de la distanță, au o caracteristică comună: sunt obținute prin programarea sistemului gazdă folosind limbaje specializate. Nivelul de abstractizare al acestor limbaje poate varia de la limbaje de descriere a mașinii de calcul, precum Verilog și VHDL, ale căror instrucțiuni sunt foarte apropiate de circuitele mașinii pe care o descriu, până la limbaje de nivel înalt, fie ele imperative, orientate obiect și/sau funcționale, precum Java, C# sau OCaml. Pentru a adresa problema continuei creșteri în dificultate a specificațiilor software, aceste limbaje trebuie să se adapteze noilor condiții, și limbaje noi, specifice domeniilor respective, trebuie proiectate și dezvoltate. În același timp, schimbările de paradigmă la nivelul proiectării hard trebuie însoțite de schimbări similare în proiectarea limbajelor. Legea lui Moore [Moo65] afirmă că numărul de tranzistoare dintr-un circuit integrat se dublează cam la doi ani. Cu toate acestea, deși se așteaptă ca această tendință să mai continue pentru 10-20 de ani (până când limitele fizice sunt atinse), implicația că dublarea numărului de tranzistoare dublează puterea de calcul serială este deja invalidată. De aceea, tranziția către arhitecturi multi-nucleu a devenit necesară: dublarea numărului de nuclee dintr-un cip conține în continuare potențialul de a dubla performanța dacă este suficient paralelism care poate fi exploatat. Pentru a putea profita de aceste arhitecturi multi-nucleu este necesară o schimbare de paradigmă în proiectarea limbajelor de programare, în care concurența cu partajarea resurselor să devină din excepție normă. Ca dovadă a acestei tendințe, unele din cele mai populare limbaje de programare sunt deja reproiectate spre a interacționa mai bine într-un mediu de

2

execuție concurent. În cazul limbajului Java, de exemplu, bibliotecile standard au fost extinse cu funcții și clase avansate pentru sincronizare și un nou model de memorie [MPA05] a fost propus pentru a permite implementări mai realistice a mașinii virtuale Java pe arhitecturile hard curente. În același timp, noul standard C++11 [ISO11] pentru limbajul C++ include în mod explicit primitive avansate pentru gestionarea și sincronizarea firelor de execuție în specificația bibliotecii standard de funcții. Cu toate acestea, necesitatea de a face limbajele suficient de flexibile pentru a putea exploata concurența fără a inhiba optimizările în procesul de compilare, poate fi satisfăcută doar prin permiterea sub-specificării și a nedeterminismului în limbaje. Acest lucru introduce provocări semnificative în procesul de testare și verificare a faptului că specificațiile sau implementările limbajelor corespund cu semantica dorită. Într-adevăr, complexitatea și lipsa uneltelor și tehnicilor potrivite pentru analiza în profunzime a propunerilor noi de definiții duce adeseori la erori subtile care sunt descoperite doar la mult timp după acceptarea lor de comunitate. De exemplu, propunerea de specificație pentru modelul de memorie x86-CC [SSN+09] a fost demonstrată neadecvată față de comportamentul pe care încerca să îl modeleze [OSS09], iar noul model de memorie Java a fost dovedit incorect pentru o parte din optimizările de compilare pe care ar fi trebuit să le permită în mod normal [SA08]. Orice limbaj de programare (existent sau viitor) are nevoie de o specificație care definește limbajul în așa fel încât utilizatorii și implementatorii să poată cădea de acord asupra înțelesului programelor scrise în acel limbaj. Această specificație constă de obicei dintr-o descriere a sintaxei limbajului, adică a construcțiilor permise de limbaj, și din semantica sa, adică comportamentul dorit al acestor constructori sintactici. Însă, deși există un consens relativ la faptul că sintaxa unul limbaj trebuie specificată formal, există mai multe feluri în care semantica limbajelor este specificată, variind de la folosirea limbajului natural (de obicei în forma unui manual), la definirea unui interpretor (numit implementare standard) sau a unui compilator al limbajului într-un alt limbaj, și până la descrierea formală a limbajului folosind limbajul matematic. Fiecare dintre abordările de mai sus are avantajele sale. De exemplu, descrierile folosind limbajul natural sunt mai accesibile, permițând practic oricui să citească specificația și să creadă că a înțeles intenția limbajului. Interpretoarele și compilatoarele permit familiarizarea cu limbajul prin testare și dezvoltarea de modele de utilizare. La rândul ei, o descriere formală a unui limbaj permite afirmarea și demonstrarea de proprietăți precise despre limbaj și programele sale. Abordările descrise au însă și limitări neneglijabile. Descrierile folosind limbajul natural sunt adeseori incomplete și uneori chiar contradictorii; pentru a obține consens în ceea ce privește înțelesul lor necesită uneori competențe de avocat în conjuncție cu cele de informatician. Interpretoarele și compilatoarele solicită familiaritatea cu limbajul țintă și pun probleme de acoperire, întrucât cazurile limită sunt de obicei mai greu de surprins prin testare; mai mult, orice extensie a limbajului, sau dezvoltarea instrumentelor de analiză, necesită de obicei o rescriere majoră (dacă nu chiar completă) a interpretorului sau compilatorului. Descrierile formale sunt limitate de puterea de expresie a limbajului de specificație folosit. Întrucât limbajele

3

de specificare se focalizează pe facilitarea exprimării trăsăturilor comune ale limbajelor de programare, ele îngreunează sau chiar fac imposibilă exprimarea în mod satisfăcător a trăsăturilor avansate ale limbajelor de programare cum ar fi schimbarea de control și sincronizarea firelor de execuție. Mai mult, fiecare limbaj de specificație pare a fi specializat pe un singur domeniu de analiză: SOS pentru semantica dinamicii execuției, semantica naturală pe analiza sistemelor de tipuri, semantica bazată pe contexte de evaluare pentru demonstrarea corectitudinii tipurilor, semantica axiomatică pentru verificarea corectitudinii programelor, și așa mai departe. În acest context, obiectivul principal al cercetării propuse prin acest proiect a fot realizarea unei platforme de lucru care să permită definirea formală a limbajelor de programare care să încorporeze toate avantajele abordărilor precedente și să elimine punctele slabe ale fiecărei dintre aceste abordări. Acest obiectiv a fost atins prin proiectarea și dezvoltarea platforme K, cunoscută sub numele K Framework (http://www.kframework.org/). Realizarea platformei K a plecat de la scopul de a arăta că se poate menține un echilibru între simplitate și puterea de expresie și analiză, fără a compromite aspectul formal. Rezultate obținute în acest proiect arată cum definițiile formale executabile pot ajuta la soluționarea problemelor formulate mai sus, mai întâi prin oferirea unui cadru matematic pentru proiectarea limbajelor de programare, apoi prin permiterea experimentării ușoare a schimbărilor asupra acestor definiții prin testare efectivă, și prin permiterea explorării și abstractizării execuțiilor nedeterministe în scopul analizării lor. Platforma are toate caracteristicele menționate în propunerea inițială a proiectului:

● este generică. Setul de limbaje de programare definite până acum în K aparțin celor mai diverse paradigme de programare: programare imperativă, programare orientată-obiect, , limbaje de asamblare, programare funcțională, programare logică, limbaje de modelare, limbaje algoritmice peste structuri de date abstracte, sisteme pentru tipuri (type systems).

● este bazat pe o semantică formală. Modelul matematic asociat unui program scris într-un limbaj specificat în K este un sistem tranzițional care descrie toate execuțiile posibile. Regulile însăși sunt formule într-un sistem logic cu sintaxă și semantică bine definită, logica accesibilității (reachability logic).

● specificațiile K sunt executabile. O componentă a suitei de unelte K transformă o specificație K într-un program care poate fi apoi utilizat, împreună cu sistemul Maude, pentru execuția de programe scrise în limbajul specificat. Utilizarea sistemului Maude nu este transparentă utilizatorului; o altă componentă din suita de unelte este Krun care facilitează execuția acestor programe. Executabilitatea este foarte importantă pentru validarea unei definiții: execuția unui număr de programe și compararea ieșirilor produse de specificație cu cea așteptată poate da încredere că limbajul definit este și cel dorit. În plus, implementări ale limbajelor pot fi testate pentru conformanță cu specificația formală a acestuia.

● specificațiile K sunt modulare. Principala caracteristică a definițiilor K care facilitează modularitatea este dată de abstractizarea configurațiilor: scriind regulile cu informație

4

minimală despre configurații, permite ca acestea sa poată fi utilizate în mai multe definiții. Modularitatea este exemplificată de limbajul CinK [LS12], un nucleu al limbajului C++, care este definit în câteva iterații. Configurația pentru iterația care definește firele de execuție este cu totul diferită de cea din iterația de bază, peste care este definită semantica firelor. Regulile definite în iterația de bază pot fi aplicate fără nici o modificare peste noua configurație. Descrierea modulară a definițiilor, permite utilizarea aceluiași modul în mai multe definiții. Mergând la extrem, putem obține un nou limbaj combinând module de la deja definite și diferite.

● K Tool oferă suport pentru concurență. Sistemul tranzițional complet dat de modelul teoretic al unu program este foarte costisitor de construit datorite dimensiunii foarte mari. În schimb se pot construi aproximări ale acestuia. Regulile pot fi etichetate iar aceste etichete pot fi date ca valoare pentru opțiunea --transition a compilatorului. Ori ce regulă cu o astfel de eticheta va genera o tranziție ori de câte ori este aplicată. Sistemul tranzițional poate fi analizat cu algoritmi de model checking sau cu suportul pentru calcul simbolic.

● K permite definirea de trăsături complexe de limbaj cum ar fi polimorfism, diferite mecanisme de legare a parametrilor formali la argumentele actuale, callcc, relația ”sequnced before” din C și C++. De asemenea poate pune în evidență programe cu semantică nedefinită.

● K Framework este o bază de raționament pentru limbaje și programe. Proiectarea logicii potrivirilor (Matching Logic) și logicii accesibilității (Reachability Logic) [RS*,RSC12] creează baze solide și cu un bun potențial pentru dezvoltarea în continuare de motoare de rescriere specializate pentru executarea definițiilor și de instrumente puternice pentru analiza și verificarea programelor. În plus, corectitudinea acestora din urmă va fi asigurată automat deoarece vor fi construite direct peste semantica limbajului. Experimentele și prototipurile construite în cadrul proiectului constituie un argument puternic pentru susținerea acestor afirmații.

Această cercetare se încadrează în proiectul de a da semantică folosind logica rescrierii, proiect propus de Meseguer și Roșu [MR04, MR06, MR07] ca un efort susținut de a dezvolta o platformă logică computațională și a instrumentelor de analiză aferente pentru proiectarea modulară a limbajelor de programare, definirea semanticii lor, analiza lor formală și implementarea lor bazată pe logica rescrierii [Mes92], cu accent pe capacitatea naturală a rescrierii de a captura concurența. Platforma K este la rândul ei bazată pe experiența câștigată din încercarea da a defini caracteristici complexe ale limbajelor de programare și din analizarea modului în care alte tehnici de definire fac față acestor situații. În particular, unele caracteristici ale platformei K sunt inspirate sau apropiate cu caracteristici de succes ale altor cadre definiționale. Reprezentarea computației ca o listă de sarcini a evoluat dintr-o reprezentare a computațiilor în interpretoarele bazate pe continuări [FWH01]. Ideea de celule și reguli structurale este asemănătoare celulelor și regulilor de încălzire/răcire folosite în Mașina Chimică Abstractă [BB92]. Ideea de a reprezenta într-o regulă doar partea din configurație necesară pentru acea regulă, lăsând detaliile să fie completate după ce toate părțile definiției au fost puse împreună, are legătură cu

5

abordarea Modular SOS [Mos04], cât și cu cea bazată pe transformări monadice [Mog91] folosită în proiectul Semantic Lego [Esp95]. Contextele de evaluare din K reprezintă același concept ca cele folosite în semantica bazată pe reducție de [WF94]. Cel de-al doilea obiectiv important al proiectului a fost ”crearea unei echipe în cadrul Universităţii Alexandru Ioan Cuza (UAIC), coordonată de Grigore Roşu (profesor asociat, angajat al Universităţii din Illinois Urbana Champaign (UIUC), SUA), în scopul proiectării şi implementării framework-ului”. Această echipă a fost format chiar de la începutul proiectului. Aceasta a fost posibilă de colaborările anterioare existente între cele două grupuri de cercetare, FSL (http://fsl.cs.illinois.edu/index.php/Main_Page) si FMSE (https://fmse.info.uaic.ro/) . Echipa a lucrat printr-o colaborare strânsă materializată prin întâlniri video pe Skype bisăptămânale, însumând în total peste 500 ore, printr-un schimb intens de mesaje email, peste 10.000, și o serie de acțiuni pentru închegarea acestei echipe și la care s-a discutat arhitectura frameworkului și s-au stabilit principalele obiective pentru etapa următoare. Prima întâlnire a avut loc în perioada 15-22 August 2010 în SUA, la Nags Head - North Carolina, sub titulatura K 2010, 1st International Workshop on the K Framework and its Applications (http://www.kframework.org/K10/). Aici a fost stabilită arhitectura versiunii 1.0 a frameworkului K, care a constat din:

● posibilitatea de a preciza sintaxa limbajului prin reguli BNF, care să fie apoi traduse în declarații Maude

● sintaxa pentru regulile semantice și posibilitatea de a preciza regulile semantice atât în notație K cât și direct în Maude

● un program ”front-end” pentru translatarea definițiilor K în Maude. Deoarece la acea fază dezvoltarea frameworkului era în stare incipientă, s-a ajuns la concluzia ca o analiză sintactică a definiției K cu expresii regulate este suficientă pentru a translata o definiție K într-o specificație MEL (Membership Equational Logic) scrisă în Maude. Din acest motiv s-a ales Perl ca limbaj pentru implementarea acestei componente. Generarea unui parser cu un generator de parsere de tip Antlr sau GOLD Parser System nu era posibilă din cauza mixării notației K cu sintaxa limbajului definit și cu sintaxa Maude (care iese din canoanele obișnuite a limbajelor de programare). Așa că s-a preferat a se utiliza parserul Maude pentru reguli, pe baza translatării regulilor de sintaxa în declarații Maude.

● Scrierea în Full-Maude a unor serii de program care să transforme specificația MEL obținută în pasul inițial într-o specificație Maude care apoi să poată fi executată, utilizând sistemul Maude, peste programe scrise în limbajul definit.

În perioada 10-15 Ianuarie 2011 s-a desfăşurat la Iaşi atelierul de lucru „Topics on the K Framework” la care au participat, pe lângă membrii proiectului, invitați din Franța și Spania. S-a prezentat stadiul curent al dezvoltării frameworkului și s-au făcut demonstrații cu limbaje definite în K. Un rezultat important al întâlnirii l-a constituit utilizarea Kului într-un proiect de cercetare INRIA, Lille. Al doilea atelier de lucru K a avut loc în perioada 8-12 August la Cheile Grădiștii, Romania (http://www.kframework.org/K11/). Aici s-au pus bazele versiunii 2.5 a frameworkului, care a

6

constat din: ● evidențierea necesității unui limbaj intermediar, KIL (K Intermediate Language) în care

să fie traduse definițiile K; ● reprezentarea codului intermediar ca o ierarhie de clase Java, ce urma să fie proiectată

în etapa următoare ● aplicarea transformărilor din backend direct peste KIL și transformarea din KIL în Maude

doar în faza finală. Al treilea atelier de lucru K a avut loc împreună cu școala de vară Summer School on Language Frameworks, Sinaia, Romania, July 23-31, 2012 (https://fmse.info.uaic.ro/events/SSLF12/). La SSLF12 K s-a confruntat cu alte abordări cu care se află oarecum în competiție: Spoofax, Rascal, Redex, Maude, Funcons. A fost un schimb de experiență foarte interesant în care fiecare abordare și-a prezentat punctele forte. Chiar dacă toate abordările au ca punct comun transformarea de limbaje, fiecare abordare a venit cu o anumită particularitate care o deosebea de celelalte, fapt ce demonstrează complexitatea domeniului și imposibilitatea de a le include pe toate într-un singur framework. K s-a evidențiat prin genericitate și amprenta dată de semantica formală executabilă. Rapoartele de progres depuse în termenele stabilite au evidențiat rezultatele obținute în fiecare din activitățile prevăzute în desfășurarea proiectului. Aceste activități au fost divizate în subactivități, cu termene periodice clare, în vederea îndeplinirii indicatorilor de realizare stabiliți în proiect. Realizarea în totalitate a acestor indicatori este prezentată în cele ce urmează.

2. Descrierea modului de îndeplinire a indicatorilor de realizare

2.1. K Framework Introdusă de Roșu [Ros03] pentru a ajuta în predarea unui curs de limbaje de programare și dezvoltată și rafinată constant până în prezent, platforma K este o platformă de definire a limbajelor de programare bazată pe logica rescrierii care pune laolaltă punctele forte ale metodologiilor existente (expresivitate, modularitate, concurență și simplicitate), evitând în același timp slăbiciunile lor. Platforma K constă in tehnica K și rescrierea K. Tehnica K poate fi —și chiar a fost deja— folosită pentru a defini limbaje de programare reale, precum Java, C, Scheme, Python, Ocaml și instrumente de analiză a programelor. Rescrierea K oferă o semantică pentru rescriere care permite mai multă concurență pentru definițiile K decât reprezentările lor directe ca teorii în logica rescrierii. Pe scurt, platforma K folosește computații, configurații și reguli K pentru a da semantică limbajelor de programare. Computațiile, de la care provine numele platformei, sunt liste de sarcini care extind sintaxa; ele au rolul de a captura partea secvențială a limbajelor de programare. Configurațiile programelor în execuție sunt reprezentate în K de mulțimi de celule imbricate, care oferă un potențial crescut de concurența și modularitate. Regulile K se disting de regulile de rescriere obișnuite prin faptul că specifică doar ceea ce este necesar dintr-o

7

configurație și pentru că identifică în mod clar ce se modifică, devenind astfel mai concise, mai modulare și mai concurente decât regulile obișnuite de rescriere.

Configurații Figura de mai sus prezintă configurația inițială a limbajului KernelC (un fragment al limbajului C). Configurația este o multi-mulțime de celule etichetate care pot fi imbricate. Fiecare celulă poate conține o listă, o multi-mulțime, o relație funcțională, sau o computație. Configurația inițială a definiției KernelC conține o celula globală, etichetată cu „T“, în care se află o mulțime de celule, printre care o celulă etichetată „mem“, care asociază valori locațiilor, o celulă listă, numită „in“, care găzduiește valorile de intrare, și o celulă multi-mulțime, numită „threads“, în care se pot afla zero sau mai multe celule „thread“ (lucru semnalat de simbolul „*“ atașat etichetei celulei). Celula thread conține și ea o multi-mulțime de celule, printre care celula „k“ conține o computație care are rolul de a dirija execuția.

Sintaxă și computații Computațiile extind sintaxa cu o operație de secvențializare a sarcinilor, „~>“. Unitatea de computație este sarcina (task), care poate fi sau un fragment de sintaxă (poate conținând goluri), sau o sarcină semantică, cum ar fi recuperarea unui context de execuție. Scrierea celei

8

mai mari părți a regulilor comune de manipulare a computației folosite în proiectarea limbajelor devine opțională, prin folosirea de adnotații sintactice intuitive precum constrângerile de strictețe care la declararea sintaxei unui constructor de limbaj specifică ordinea de evaluare a argumentelor sale. Descompuneri asemănătoare ale computației pot fi întâlnite în folosirea stivelor în mașini abstracte de execuție [FF86, FWH01] precum și în tehnicile de reorientare folosite în implementarea semanticii prin reducție cu contexte de evaluare [DN04]. Distincția provine în cazul platformei K din faptul că în K această descompunere este realizată formal, folosind reguli (adnotațiile de strictețe corespund unor reguli K structurale) și nu ca un mijloc de a obține o implementare așa cum se întâmpla în celelalte cazuri. Adnotațiile de strictețe adaugă informație semantică sintaxei, specificând ordinea de evaluare a argumentelor pentru fiecare constructor de limbaj. Regulile de încălzire/răcire asociate stricteții permit ca argumentele menționate în constrângerile de strictețe pot fi scoase din context spre evaluare în orice moment, și apoi introduse înapoi în contextul lor original. Astfel, prin reguli de strictețe, ordinea de evaluare devine o secvență de pași.

Regulile K Să considerăm următoarea funcție „swap“ pentru schimbarea valorilor a două locații date ca argumente:

void swap(int * x,int * y) { int t = * x; * x = * y; * y = t;

} Să zicem că ne aflăm în mijlocul unui apel al funcției „swap“ cu parametrii „a“ și „b“ (care sunt asociate locațiilor 4 și 5, respectiv). Să presupunem în continuare că toate instrucțiunile în afara ultimei au fost deja executate și că în acea instrucțiune variabila y a fost deja evaluată la locația 5. Configurația globală din figura de mai jos reprezintă o configurație a unui moment din execuție corespunzând acestei situații. Datorită regulilor de strictețe știm că următorul pas în execuție este evaluarea variabilei t.

9

Figura de mai sus arată cum se poate obține regula K pentru citirea valorii unei variabile locale direct din configurația pasului de execuție corespunzător. Mai întâi, printr-un proces de abstracție a conținutului celulelor, putem să ne concentrăm doar pe părțile din celule care au relevanță pentru această regula. În același timp, ne putem declara intenția de a îl înlocui pe t cu

10

locația asociată lui în celula env (care este 1); facem acest lucru subliniind partea care se schimbă și scriind termenul care o înlocuiește sub linie, prin procesul de rescriere localizată. Apoi, prin procesul de abstracție a configurației sunt păstrate doar celulele relevante, în timp ce prin procesul de generalizare instanțele concrete ale identificatorilor și constantelor sunt înlocuite cu tipurile corespunzătoare. Marginile „rupte“ sunt folosite pentru a semnala că pot fi mai multe elemente în celulă (în partea corespunzătoare) în afară de ceea ce este menționat explicit. Regula K obținută astfel descrie succint semantica intuitivă pentru citirea unei variabile locale: dacă variabila locală X trebuie evaluată la pasul următor și dacă lui X îi este asociată valoarea V în stiva locală, atunci acea apariție a lui X trebuie înlocuită cu V. Mai mult, acest lucru este obținut prin menționarea doar a părților strict necesare din configurație, fapt esențial pentru obținerea definițiilor modulare și prin identificarea precisă a părților ce se modifică, fapt care amplifică simțitor potențialul pentru concurență. Imaginile de mai sus prezintă versiunea grafică a configurațiilor și regulilor K, generată folosind utilitarul kompile în modul de generare a documentației pentru o definiție. Interfața utilizator a platformei K permite scrierea acestor reguli folosind editoare text. Iată, de exemplu, cum este reprezentată regula de mai sus în limbajul K:

Pentru a sugera ideea de celulă care îngrădește un conținut, se asociază fiecărei celule un element de tip XML cu numele acelei celule. Pentru a arăta că regula menționeaza doar un fragment din conținutul celulei, se folosește simbolul „…“ în locul în care celula este „ruptă“. În final, pentru a reprezenta ideea de rescriere locală, se folosește simbolul „=>“, care are înțelesul de a transforma partea stângă în partea dreaptă în contextul dat.

2.2 Tehnici si metodologii pentru definirea şi analiza trăsăturilor complexe de limbaj

2.2.1 Modularitate Procesul de abstracție a configurației este instrumental în atingerea nivelului de modularitate dorit în platforma K. Bazându-se pe faptul că specificarea include o configurație inițială și că de obicei structura unei astfel de configurații nu se modifică în timpul execuției unui program, regulile K sunt invariabile la schimbările de structură ale configurației. Practic, acest lucru înseamnă că aceeași regulă poate fi refolosită în definiții diferite cu condiția ca celulele specificate să fie prezente, indiferent de contextul adițional, care poate fi dedus automat din configurația inițială. De exemplu, limbajul CinK este definit incremental, în mai multe iteraţii. Regulile din iteraţia de bază pot fi executate şi peste extensia cu fire de execuţie, unde configuraţia limbajului este modificată pentru a gestiona execuţiile concurente ale firelor (a se vedea mai jos).

11

2.2.2 Apel cu continuare curentă Structura aparte a computațiilor K, incluzând faptul că sarcina curentă este tot timpul în vârful computației, sporește foarte mult expresivitatea platformei K. Un exemplu în acest sens este semantica instrucțiunii apel cu continuarea curentă (call/cc), care este prezentă în câteva limbaje funcționale (precum Scheme), și într-o anumită măsură în unele limbaje de programare imperative (cum ar fi instrucțiunea longjmp în C). Call/cc este recunoscută ca fiind greu de capturat de majoritatea metodologiilor (cu excepția semanticii folosind reducție cu contexte de evaluare) datorită imposibilității lor de a avea acces la contextul execuției, care este capturat la meta-nivel de contextul logic și de aceea nu poate fi observat la nivel logic. Deoarece în definițiile K tot restul computației se află după sarcina curentă de execuție, această instrucțiune poate fi capturată în mod succint de următoarele două reguli:

Prima regulă „împachetează“ într-o valoare restul curent al computației și o pasează argumentului instrucțiunii „callcc“, care trebuie să fie o funcție. Dacă în timpul evaluării acelei funcții valoarea-computație este aplicată unei valori atunci restul computației la acel moment este înlocuit de computația salvată, căreia îi este prefixată valoarea dată ca argument (ca rezultat al expresiei callcc originale). 2.2.2 Sincronizare O altă situație greu de reprezentat folosind alte tehnici este manipularea mai multor sarcini concomitent, ca de exemplu în cazul definirii comunicării sincrone. Deși formalismele bazate pe SOS pot captura versiuni particulare ale acestei paradigme pentru limbaje ca CCS sau π-caculus, ele pot face asta doar pentru că acolo primitivele de comunicare se află mereu la vârful proceselor. Structura computațiilor K este folositoare și în acest caz, permițând accesul la doi pași concurenți de execuție în același timp, așa cum se vede în regula următoare, care definește schimbarea sincronă a mesajelor într-un mediu multi-agent:

12

O lectură a regulii este de ajuns pentru a înțelege semantica dorită: dacă un agent, identificat prin N1 încearcă să trimită un mesaj unui agent identificat prin N2 și dacă acel agent așteaptă să primească un mesaj de la N1, atunci instrucțiunea de trimitere este dizolvată în primul agent, în timp ce expresia de primire din agentul care recepționează e înlocuită de valoarea trimisă. 2.2.3 Concurență O altă caracteristică care face platforma K potrivită pentru definirea limbajelor de programare este modul ei natural de a captura concurența. În completarea faptului că platforma K oferă, asemenea mașinii chimice abstracte, concurență adevărată și astfel atinge scopul menționat mai sus pentru o platforma ideală, regulile K permit și concurență cu partajarea resurselor. Să exemplificăm această concurență. Regulile de mai jos sunt regulile KernelC pentru citirea/scrierea unei valori la o locație de memorie:

13

Să considerăm mai întâi o configurație în care două fire de execuție, specificate prin două celule de computație sunt gata simultan să citească valoarea aceleiași locații de memorie:

Întrucât semantica regulilor K spune că părțile din configurație care nu sunt modificate de regulă pot fi partajate de aplicațiile concurente ala regulii (în acest caz constructorul asociat celulei de memorie și cel de asociere a locației 3 la valoarea 1), regula de citire poate fi instanțiată pentru ambele fire de execuție și amândouă pot avansa într-un pas concurent. La fel se întâmplă și în cazul modificărilor concurente. Cât timp firele de execuție încearcă să scrie în locații diferite de memorie, regula de rescriere poate fi instanțiată simultan și firele de execuție pot avansa într-un pas concurent:

14

Mai mult, prin interzicerea suprapunerii instanțelor de reguli pe părțile care se schimbă, semantica K forțează secvențializarea accesului concurent la aceeași locație (când unul din accese e de scriere), așa cum se vede în figura de mai jos:

Acest model de semantică concurentă pentru limbajul K se obține printr-o reprezentare a rescrierii concurente K ca instanță a unui proces concurent de rescriere prin intermediul

15

grafurilor. Mai multe detalii despre această codificare pot fi găsite în monografia [Șer12] și în articolul de conferință [ȘR12]. 2.2.4 Model-checking Definirea firelor de execuție este inclusă în câteva limbaje: IMP++, Simple, Cink. Exemplificăm definiția firelor de execuție în Cink (un nucleu al limbajului C++) [LS13] (definiţia completă a iteraţiei cu fire de execuţie se găseşte pe situl proiectului: https://github.com/kframework/cink-semantics/tree/master/threads). Trei paşi importanți sunt necesari pentru adăugarea firelor de execuţie: - sintaxa

- adăugarea la configuraţie de celule care să permită crearea unui număr nelimitat de fire de execuţie

În configuraţia de mai sus avem o celulă threads care include yero, una sau mai multe celule thread. Fiecare celulă thread include subconfiguraţia corespunzătoare a unui fir de execuţie. Astfel, fiecare fir de execuţie își are propria celulă de computaţii k, o celulă env pentru gestionarea variabilelor locale, propria stivă pentru apelurile de funcţii şi propriile side-efect-uri (specifice limbajelor C şi C++). - adăugarea de reguli pentru operaţii cu fire de de execuţie. De exemplu crearea unui fir se face cu o regulă de forma

16

Pentru noul fir sunt precizate numai conţinuturile celulelor cu informaţie specifică, celelalte celule având valorile implicite din declaraţia configuraţiei. Terminarea uni for printr-o regulă de forma

Un thread se termină când celula de computații k este vidă. Programele concurente pot fi verificate cu algoritmi de model-checking în cazul când spaţiul configuraţiilor concrete generate de execuţiile posibile ale programului este finit. Proprietăţile verificate sunt formule LTL. Propoziţiile atomice sunt definite printr-o sintaxă de forma:

Funcţia de etichetare a configuraţiilor B cu propoziţii atomice P este dată printr-o relaţie de satisfacere semantică B╞ P, relaţie definită prin reguli de forma

17

unde val(B, X) este o funcţie auxiliară (definită tot în K) ce întoarce valoarea variabilei program X în configuraţia B. Apelarea model-checkerului este exemplificată în secţiunea dedicată utilitarului krun. 2.2.5 Obiecte și clase Metodologia de definire a obiectelor şi claselor este descrisă în secţiunea dedicată definiţiei K a limbajului Java. Aceasta este similară cu cea descrisă în KOOL (definiţia cestui limbaj poate fi găsită la adresa https://github.com/kframework/k/tree/master/tutorial/2_languages/2_kool), limbaj cu caracter mai mult didactic pentru predarea conceptelor OO ale limbajelor de programare. 2.2.6 Semantica statică Semantica statică (sau sistemul de tipuri) pentru un limbaj poate fi definită într-o manieră similară cu cea semanticii limbajului. Vom considera ca exemplu semantica statică a limbajului IMP++ (definiţia completă este descrisă în tutorialul 5.1, care poate fi vizionat la adresa http://www.kframework.org/index.php/Lesson_1,_Type_Systems:_Imperative,_Environment-Based_Type_Systems). Rezultatele pentru semantica statică sunt tipuri:

Configuraţia are o structură mult mai simplă, formată doar din două celule deoarece acum interesează numai tipurile pentru variabile:

Evaluarea unei variabile constă în înlocuirea acesteia cu tipul asociat:

Semantica unei atribuiri constă în atribuirea tipului expresiei din dreapta variabilei din partea stângă:

18

Evaluarea unui operator constă în calculul tipului rezultat:

Execuţia unei instrucţiuni va produce tipul asociat:

Doar instrucţiunea bloc are o semantică mai specială deoarece presupune salvarea stării curente a variabilelor:

2.2.7 Platforma de execuție simbolică independentă de limbaj În cadrul mediului de dezvoltare K a fost dezvoltată și o platformă care permite execuția simbolică a programelor [ALR13b]. Practic, ideea generală a fost aceea de a oferi utilizatorilor K nu doar posibilitatea de a rula programele în mod obișnuit ci și de a le executa simbolic. Execuția simbolică permite rularea unui program care manipulează atât date de intrare concrete cât și date de intrare simbolice, a căror valoare nu este cunoscută. Să considerăm spre exemplu următorul program: int n, sum; n = 100; sum = 0; while (!(n <= 0)) {

19

sum = sum + n; n = n + -1; } Acest program calculează suma primelor n numere, unde n este 100 (valoare concretă). La momentul execuției acestui program folosind semantica K a limbajului obținem: $ krun sum.imp <T> <k> .K </k> <state> n |-> 0 sum |-> 5050 </state> </T> După cum se poate observa din configurația finală, suma calculată în variabila sum este exact valoarea așteptată 5050. Execuția simbolică presupune utilizarea de valori simbolice în locul celor concrete, rezultatul execuției fiind o constrângere a unui drum de execuție în program. Acelaşi program cu valori simbolice de intrare (aici valoarea iniţială a lui n) poate fi scris sub forma int n, sum; n = N:Int; sum = 0; while (!(n <= 0)) { sum = sum + n; n = n + -1; } unde N:Int este o valoare simbolică ce poate desemna orice număr întreg. Execuţia simbolică va putea explora execuţiile programului pentru toate valorile posibile ale lui N:Int. Implementarea metodologiei este descrisă în 2.3.3.

2.3 K tool - utilitar suport pentru K framework Pentru a avea mai mult control asupra definițiilor, framework-ul K a fost împărțit în patru mari componente cu diferite scopuri: - kompile - preia la intrare o definiție K, din care generează o serie de fișiere necesare pentru parsarea și execuția de programe; - kast - preia la intrare un program pe care îl parsează și afișează rezultatul sub forma de KAST (K Abstract Syntax Tree - limbajul intern, intermediar framework-ului); - krun - este instrumentul care în final combină rezultatul compilării definiției și parsării de programe pentru a executa programe; - ktest - oferă utilizatorului o modalitate de a compila, rula și testa o serie de definiții și programe pentru a automatiza și fluidiza procesul de verificare a codului scris. Framework-ul K este distribuit sub forma de arhivă în care sunt grupate pe categorii elementele

20

necesare rulării instrumentelor. Folosind structura standard de fișiere pentru proiecte UNIX, utilizatorul poate identifica rapid elementele necesare pentru dezvoltarea unei definiții. Astfel directoarele /bin și /lib sunt destinate exclusiv dezvoltatorilor și conțin scripturile de rulare și programele intermediare necesare compilării și rulării definițiilor și programelor. Directoarele /samples și /tutorial includ o serie de definiții ajutătoare în care sunt explicate principiile de bază din teoria framework-ului. Directorul /include conține toate elementele de sintaxă care pot fi folosite de utilizatori în definițiile de limbaje. Conțin operațiile peste întregi, numere reale, operații peste șiruri de caractere, precum și o serie de operații de nivel înalt precum liste, tabele asociative, mulțimi. 2.2.1 kompile Utilitarul kompile este cea mai complexă componentă din suita de unelte K. Funcționalitățile de bază ale utilitarului includ translatarea unei definiții K într-o specificație executabilă și generarea de parsere pentru limbajul pentru cazul când sintaxa limbajului este definită tot în K. Definițiile K pot fi date și cu ajutorul unui parser extern (a se vedea descrierea definiției limbajului Java de mai jos). Compilarea unei definiții se face prin apelarea utilitarului kompile și dând ca parametru numele fișierului care include definiția limbajului: $ ls README exercises imp.k tests $ time kompile imp real 0m26.106s user 0m34.965s sys 0m1.059s În compilarea de mai sus a limbajului IMP din tutorial s-a listat și timpul de compilare. Deși definiția limbajului este mică, compilarea a durat mai mult de 30 secunde. Aceasta demonstrează volumul de calcul necesitat de o compilare. Definiția compilată se află în directorul imp-kompiled: $ ls README imp-kompiled imp.pdf exercises imp.k tests $ ls imp-kompiled/ base.maude consTable.txt ground builtins.maude def main.maude configuration.bin defx-maude.bin pgm Programele Maude includ specificația executabilă generată de compilator. În afară de acestea, compilatorul mai generează trei parsere: unul pentru programe IMP, care se află în directorul pgm, unul pentru parsarea de termeni K+IMP fără meta-variabile (ground terms), care se află în directorul ground, și unul care poate parsa orice termen K+IMP (inclusiv cu meta-variabile), care se află în directorul def. Compilatorul utilizează SDF ca instrument de bază de parsare. Primul pas al compilării constă în generarea de specificații SDF din definiția limbajului. Din specificația SDF a limbajului și cea

21

a K-ului este generată o tabelă de parsare; acest pas este cel mai mare consumator de timp. Această tabelă este apoi parsată de către utilitarul SGLR (ambele componente sunt parte ale SDFului), care generează un arbore de parsare ambiguu în formatul ATerm. Un algoritm complex, bazat pe inferență de sorturi și care ține cont de caracterul particular al definiției K-ului, dezambiguizează arborele de parsare și generează o formă intermediară a definiției K; limbajul intermediar de reprezentare se numește KIL (K Intermdiate Language) și este implementat de o ierarhie de clase Java. Reprezentarea KIL a definiției este apoi transformată de o succesiune de pași într-o mașină virtuală, care e descrisă într-un nucleu al limbajul K, numit KORE. Această mașină virtuală are proprietatea că poate fi ușor interpretată în diferite backend-uri. Unul dintre aceste backend-uri este Maude. Utilizarea lui este descrisă de secțiunea dedicată utilitarului krun. K a aderat la principiul ”literate programming” formulat de Donald Knuth, care constă în completarea definiției cu comentarii descrise în limbaj natural. Utilizând backendul pdf se poate genera un fișier pdf care să includă versiunea ”citibilă” a definiției (în exemplu de mai jos comentariile au fost eliminate pentru a economisi spațiu: Dorels-MacBook:lesson_4 dlucanu$ kompile imp --backend pdf Versiunea pdf a definiției limbajului IMP poate fi vizualizată cu orice utilitar capabil să manipuleze fișiere pdf: Dorels-MacBook:lesson_4 dlucanu$ open imp.pdf

22

23

24

Alte backend-uri sunt: latex, symbolic (descris într-o secțiune separată în acest document), html, unparse (listează versiunea intermediară obținută după un anume pas de compilare dat ca parametru). Comanda kompile include și alte opțiuni:

● -h,--help: afișează un mesaj de help, împreună cu opțiunile existente ale toolului ● --version: afișează informații despre versiune . ● -v,--verbose: afișează informații suplimentare referitoare la starea actuală din momentul compilării ● d,--directory <dir>: specifică calea către directorul în care se găsește definiția compilată . Ieșirea

poate fi fie o definiție K compilată, fie un document ce depinde de tipul back-endului. Implicit este directorul curent.

● --backend <backend>: Alegerea unui backend. <backend> este unul dintre pdf|latex|html|maude|java|unparse|symbolic]. Fiecare din pdf|latex|html generează un document din definiția K în cauza. Opțiunea maude|java crează definiția K compilată. unparse generează o versiune neparsată a definiției K iar simbolic generează semantica simbolică.

● --doc-style <string/file>: Specifică o opțiune de stil pentru pachetul k.sty (când se folosește '--backend [pdf|latex]' ) sau calea pentru un fișier .css dacă se folosește '--backend html '.

● -w,--warnings <all|none> : Nivelul de avertizare. Implicit: none. ● --main-module <string> : Modulul main în care un program începe execuția. Informația

este folosită de krun. Implicit este numele fișierului ce conține definiția K fără extensia .k. ● --syntax-module <string> : Modulul main pentru sintaxă. Informația este folosită de krun.

(Implicit este main-module>-SYNTAX). ● --superheat <string> : Specifică construcția sintactică ce realizează superheat pentru

calcul. Se folosește în combinație cu --supercool. <string> este o listă de taguri de producții

25

depărțite prin virgulă. ● --supercool <string> : Specifică ce reguli realizează supercool pentru calcule. Se

folosește împreună cu --superheat. <string> este o listă de taguri de producții depărțite prin virgulă.

● --transition <string>: <string> este o listă de taguri despărțite prin virgulă, care desemnează reguli ce urmează a deveni tranziții.

● -X,--help-experimental : Afișează help pentru opțiuni nonstandard. Printre aceste opțiuni experimentale (care nu sunt standard) se numără:

● --step <string> : Numele fazei de compilare după care procesul de compilare trebuie să se oprească.

● --lib <file> : Specifică biblioteci suplimentare pentru compilare/execuție. ● --add-top-cell: Se adaugă o celulă la configurație și la reguli. ● --kcells <string>: Celule care conțin computații. ● --sort-cells: Sortarea celulelor conform ordinii din configurații. ● --smt <solver>: Solverul SMT utilizat pentru verificarea constrângerilor.

<solver> este unul din [z3|none]. (Default: z3). Opțiunea are efect doar cu '--backend symbolic '. ● --fast-kast: Utilizarea parserului experimental rapid C SDF. ● --symbolic-rules <tags>: Se aplică transformările simbolice doar regulilor adnotate cu

taguri din <tags> set. Opțiunea are efect doar cu '-backend symbolic'. ● --non-symbolic-rules <tags> : Nu se aplică transformările simbolice regulilor adnotate cu

taguri din <tags> set. Opțiunea are efect doar cu '-backend symbolic'. 2.3.2 krun O altă componentă importantă a suitei de utilitare K este krun, care utilizează specificația Maude executabilă a unei definiții K pentru a executa programe scrise în limbajul definit. Utilitarul krun apelabil la linia de comandă furnizează următoarele opțiuni:

● -h,--help: afișează un mesaj de help, împreună cu opțiunile existente ale toolului ● --version: afișează informații despre versiune: este prezentată versiunea de git și data de build ● -v,--verbose: afișează informații suplimentare referitoare la starea actuală din momentul rulării ● d,--directory <dir>: specifică calea către directorul în care definiția compilată se găsește. Implicit

este folderul curent ● --main-module <name>: specifică modulul principal în care un program începe să se execute.

Implicit este modulul specificat în definiția K furnizată ● --syntax-module <name>: specifică modulul principal pentru sintaxă. Implicit este modulul specificat

în definiția K furnizată ● --io <[on|off]>: indică dacă să se utilizeze operații IO reale atunci când se execută o definiție. În

mod implicit această opțiune este activată ● --color <[on|off|extended]>: specifică dacă să se utilizeze culori la ieșire, pentru o colorare

care să scoată în evidență tipurile de celule existente ● --terminal-color <color-name>: indică culoarea de fundal a terminalului. Celulele nu vor fi

colorate în această culoare. Valoarea implicită este negru ● --parens <[greedy|smart]>: selectează algoritmul de inserare a parantezelor. Valoarea implicită

este ’greedy’��. Valoarea ’smart’�� poate lua mai mult timp de execuție ● --parser <command>: comandă utilizată pentru a parsa programe. Permite utilizarea tool-ului

împreună cu un parser extern (implicit este kast)

26

● --config-var-parser <file>: comandă utilizată pentru a parsa variabile de configurație. Implicit este kast -�-e. A se vedea opțiunea --��parser de mai sus. Se aplică la opțiuni --��c ulterioare până când un alt parser este specificat cu această opțiune

● -c,--config-var <name=value>: specifică valori pentru variabilele din configurație ● -o,--output <mode>: specifică cum să se afișeze rezultatele Maude. Argumentul <mode> poate lua

una din următoarele valori: [pretty|raw|binary|none]. Valoarea implicită este pretty, când configurația finală este afișată frumos, cu indentări și spațieri corespunzătoare pentru a se ilustra mai bine înlănțuirea, imbricarea și conținutul diferitelor tipuri de celule

● --search: În legătură cu această opțiune se pot specifica alte 3 opțiuni care sunt opționale: pattern (șablonul utilizat pentru căutare), bound (numărul de soluții dorite) și depth (adâncimea maximă a căutării)

● --search-final: la fel ca și opțiunea –search numai că returnează numai stările finale, chiar dacă opțiunea --depth este specificată

● --search-all: la fel ca și opțiunea –search, dar returnează toate stările care se potrivesc, chiar dacă opțiunea --depth nu este furnizată

● --search-one-step: la fel ca și –search, dar caută numai un singur pas de tranziție ● --search-one-or-more-steps: la fel ca și –search-all, dar exclude starea inițială, chiar dacă se

potrivește ● --pattern <string>: specifică un termen și/sau o condiție a cărui rezultat al execuției sau căutări

trebuie să se potrivească pentru a reuși. Returnează potrivirile rezultate ca o listă de substituții. În legătură cu aceasta se pot specifica alte 2 opțiuni care sunt opționale: bound (numărul de soluții dorite) și depth (adâncimea maximă a căutării)

● --bound <num>: numărul de soluții dorite pentru căutare ● --depth <num>: numărul maxim de pași computaționali pentru care să se efectueze o execuție sau

căutare în definiție ● --graph: afișează graful de căutare generat de către ultima căutare ● --backend <backend>: specifică backendul de krun cu care să se execute un program. Valorile

disponibile sunt: maude și java. Valoarea implicită este maude ● -X,--help-experimental: afișează helpul pentru o serie de opțiuni care nu sunt standard ● --simulation <string>: proprietate de simulare a două programe în două semantici

Printre aceste opțiuni experimentale (care nu sunt standard) se numără:

● --fast-kast: specifică utilizarea parserului C SDF care este mai rapid ● --statistics <[on|off]>: afișează statisticile din rescrierea Maude ● --term <string>: argumentul de intrare va fi parsat cu parserul specificat și utilizat ca singurul input

la krun ● --maude-cmd <string>: comanda Maude utilizată pentru a executa definiția ● --log-io <[on|off]>: determină ca serverul IO să creeze loguri. Implicit este dezactivată această

opțiune ● --debug: rulează o execuție în modul debug ● --debug-gui: rulează o execuție în modul debug, oferind în plus o interfață grafică pentru o vizualizare

și investigare mai facilă a execuției în modul debug ● --debug-info: furnizează informații de debugging ● --trace: activează maude trace ● --profile: activează maude profiler ● --ltlmc <file/string>: specifică formula pentru model-checker prin intermediul unui fișier sau la

linia de comandă ● --prove <file>: demonstrează un set de reguli de accesibilitate ● --smt <solver>: solverul SMT utilizat pentru verificarea constrângerilor. Poate lua una din valorile:

z3|gappa|none. Valoarea implicită este z3 ● --generate-tests: programele de test vor fi generate pe parcursul căutării normale

27

De asemenea utilitarul krun include facilități care să permită raportarea și corectarea erorilor prin intermediul funcționalității de stepper/debugger. Astfel este posibilă rezumarea/întreruperea la un anumit punct din execuția programului și vizualizarea configurației parțiale. Utilizatorul poate corecta sau modifica configurația și rula ulterior programul ținând cont de aceste noi informații specificate. De asemenea este inclusă posibilitatea de a adăuga adnotări de tip “label” la nivelul setului de reguli din semantică pentru a stopa execuția programului la un anumit pas.

Opțiunile disponibile în funcționalitatea de debug sunt următoarele:

● --help: afișează comenzile disponibile ● --step: se execută un singur pas sau mai mulți pași la un singur moment de timp dacă se specifică un

număr întreg pozitiv ● --step-all: calculează toți succesorii în una sau mai multe tranziții (dacă se specifică un număr

întreg pozitiv) a configurației curente ● --select <number>: selectează configurația curentă după un rezultat de căutare utilizând comanda

step-all ● --show-search-graph: afișează graful de căutare generat de către ultima căutare ● --show-node <NODE>: afișează informații despre nodul specificat în graful de căutare. Nodul este

specificat prin id-ul său ca argument al acestei opțiuni ● --show-edge <NODE1 NODE2>: afișează informații despre muchia specificată în graful de căutare.

Muchia este specificată prin id-urile extremităților sale indicate ca argument în această opțiune ● --resume: rezumă execuția și iese din modul debug ● --abort: încheie execuția și iese din modul debug ● --save <STRING>: salvează sesiunea de debug într-un fișier ● --load <STRING>: încarcă sesiunea de debug dintr-un fișier ● --read <STRING>: citește un string de la stdin

Exemple de scenarii de utilizare a interpretorului krun ● Ilustrare a comenzii --output=none: - compilare a limbajului imp.k din folderul k/tutorial/1_k/4_imp++/lesson_7 (https://github.com/kframework/k/blob/master/tutorial/1_k/4_imp%2B%2B/lesson_7/imp.k): kompile imp.k - rulare a unui program interactiv io.imp (în care se cere input de la utilizator): krun ../lesson_1/tests/io.imp --output=none Exemplu de output (dacă se introduc de la tastatură numerele 3 și 8): Input two numbers: 3 8 Their sum is: 11 Dacă același program s-ar fi rulat fără a se mai preciza opțiunea --output=none, outputul rezultat în urma rulării ar fi fost cel de mai jos, în care pe lângă afișarea sumei rezultate dintre cele 2 numere introduse, mai apare și configurația finală rezultată: krun ../lesson_1/tests/io.imp

Input two numbers: 3 8

28

Their sum is: 11 <T> <in> ListItem(#buffer ( "" )) ListItem(#istream ( 0 )) </in> <out> ListItem(#ostream ( 1 )) ListItem(#buffer ( "" )) </out> <threads> <thread> <k> .K </k> <id> 0 </id> <env> x |-> #symNat(2) y |-> #symNat(3) </env> </thread> </threads> <store> #symNat(2) |-> 3 #symNat(3) |-> 8 </store> </T>

● Ilustrare a comenzii --ltlmc: Prin intermediul acestei opțiuni se verifică validitatea unor formule LTL cu ajutorul interpretorului krun. Formula poate fi furnizată atât direct ca argument al opțiunii, cât și în cadrul unui fișier. În cazul în care formula este satisfăcută se va afișa la output true, iar în caz contrar va fi furnizat în mod pretty printed contra-exemplul care arata execuția care duce la starea care violează proprietatea. - compilare a limbajului cink.k din definiția cink-semantics, un nucleu al limbajului C++, (https://github.com/kframework/cink-semantics), extinsă cu facilitatea de a specifica propoziții atomice satisfăcute de configurații (detalii în definiţia completă https://github.com/kframework/cink-semantics/tree/master/ltlmc): kompile cink --transition="kripke" - rulare cu comanda (formula este introdusă direct de la linia de comandă): krun programs/dekker.cink --ltlmc "[]Ltl ((eqTo(critical1, 1) ->Ltl eqTo(critical2, 0)) /\Ltl (eqTo(critical2, 1) ->Ltl eqTo(critical1, 0)))" Programul dekker.cink ilustrează algoritmul lui Dekker pentru excludere mutuală. După execuţia comenzii de mai sus se va afișa

29

true ceea ce arată faptul că formula este satisfăcută; - o comandă de execuție echivalentă cu cea de mai sus este următoarea: krun programs/dekker.cink --ltlmc programs/form-dekker.cink în care formula de verificat se găsește în fișierul form-dekker.cink în acest caz, outputul ar fi fost același și anume: true - dacă pentru rulare se va folosi comanda: krun programs/peterson-wrong1.cink --ltlmc "[]Ltl ((eqTo(critical1, 1) ->Ltl eqTo(critical2, 0)) /\Ltl (eqTo(critical2, 1) ->Ltl eqTo(critical1, 0)))" se vor furniza mai multe contraexemple (mai jos este ilustrat doar o parte din acestea):

Vertices:<T> <in> ListItem(#buffer ( "" )) ListItem(#istream ( 0 )) </in> <out> ListItem(#ostream ( 1 )) ListItem(#buffer ( "" )) </out> <threads> <thread> <k> $update ( #symScalLoc(1) , 1 ) ~> lval ( #symScalLoc(1) ) ~> HOLE ; ~> ((int critical1) ;) ((critical1 = 0) ;) ~> (( int critical2) ;) ((critical2 = 0) ;) ~> (int peterson1) ( .Decls ) { (while ( true ) ({ ((((while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ; )) })) } ~> (int peterson2) ( .Decls ) { (while ( true ) ({ ((((while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) (( turn = 1) ;)) ((critical2 = 0) ;)) })) } ~> (int main) ( .Decls ) { ((std::thread t1 ( peterson1 , '.Exps(.KList) ) ; ) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute </k> <return> .K </return> <name> noName </name> <fstack> .List </fstack> <sideEffects> .Bag

30

</sideEffects> <env> turn |-> #symScalLoc(1) </env> </thread> </threads> <store> #symScalLoc(1) |-> 0 </store> <genv> .Map </genv> </T>,<T> ...

Programul peterson-wrong1.cink reprezintă o versiune incorectă a algoritmului lui Peterson pentru excludere mutuală; ● Ilustrare a comenzii --search: - compilare a limbajului cink.k, din semantica cink-semantics, folderul basic

(https://github.com/kframework/cink-semantics/tree/master/basic): kompile cink --superheat="plus" --supercool="mem-lookup return" - rulare a programului print.cink folosind comanda --search împreună cu opțiunea --bound, care în cazul de mai jos limitează numărul de soluții afișate la 4: krun programs/print.cink --search --bound=4 Programul print.cink constituie un exemplu de program care manifestă un comportament ne-deterministic a unui program definit. Mai jos este ilustrată doar prima soluție găsită: Search results:

Solution 1: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "132" )) </out> <control> <k> .K </k> <return> 6

31

</return> <fstack> .List </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(2) print |-> #symScalLoc(1) </env> </control> <genv> main |-> #symScalLoc(2) print |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( (int n) @ (((cout << n) ;) (return n ; )) ) #symScalLoc(2) |-> lambda ( .Decls @ (return (((print ( 1 )) + (print ( 2 ))) + (print ( 3 ))) ;) ) #symScalLoc(3) |-> 1 #symScalLoc(7) |-> 3 #symScalLoc(8) |-> 2 </store> </T>

● Ilustrare a comenzii --debug: - compilare a limbajului cink.k, din semantica cink-semantics, folderul basic

(https://github.com/kframework/cink-semantics/tree/master/basic): kompile cink --transition "side-effect assign" - rulare a programului undefined.cink, care manifestă un comportament nedefinit: krun programs/undefined.cink -cIN="ListItem(#symInt(n))" -cPC="true" --debug Prin intermediul opțiunii --debug se va intra în modul de execuție debug, iar la output se va afișa: After running one step of execution the result is:

Node 1: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k>

32

x = 1 ~> HOLE ; ~> (x = ((x ++) + 1)) ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 0 </store> </T>

urmând să fie afișată în continuare o linie de comandă internă debuggerului (Command >), de unde se pot introduce o serie de opțiuni specifice, ce pot fi aflate folosind comanda --help. Dacă în continuare, în modul debug de execuție se introduce comanda step 3 se va afișa: Command > step 3

Node 4: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k> x = ((x ++) + 1) ~> HOLE ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; )

33

</fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 1 </store> </T>

introducerea comenzii step-all 2 va produce următorul output (doar o parte este ilustrată): Command > step-all 2

Search results:

Solution 1: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k> (lval ( #symScalLoc(2) )) = ((x ++) + 1) ~> HOLE ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env>

34

</control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 1 </store> </T>

pentru aflarea unor informații suplimentare despre nodul cu id-ul 3 din graful de căutare se va utiliza comanda show-node 3: Command > show-node 3 Node 3: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k> (lval ( #symScalLoc(2) )) = 1 ~> HOLE ; ~> (x = ((x ++) + 1)) ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 0 </store>

35

</T> iar pentru aflarea unor informații suplimentare în privința muchiei ce conectează nodurile cu id-urile 4 și 6, se va folosi comanda Command > show-edge 4 6 Node 4: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k> x = ((x ++) + 1) ~> HOLE ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 1 </store> </T> => Node 6: <T> <in> ListItem(#buffer ( "\n" )) </in> <out>

36

ListItem(#buffer ( "" )) </out> <control> <k> lval ( #symScalLoc(2) ) ~> HOLE = ((x ++) + 1) ~> HOLE ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack> ( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> .Bag </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 1 </store> </T> dacă se dorește în continuare selectarea nodului 10, se va utiliza comanda select 10: Command > select 10 Node 10: <T> <in> ListItem(#buffer ( "\n" )) </in> <out> ListItem(#buffer ( "" )) </out> <control> <k> x = 2 ~> HOLE ; ~> return x ; ~> return noVal ; </k> <return> .K </return> <fstack>

37

( ([ main |-> #symScalLoc(1) ]) , HOLE ; ) </fstack> <sideEffects> <sideEffect> $inc ( #symScalLoc(2) , 1 ) </sideEffect> </sideEffects> <env> main |-> #symScalLoc(1) x |-> #symScalLoc(2) </env> </control> <genv> main |-> #symScalLoc(1) </genv> <store> #symScalLoc(1) |-> lambda ( .Decls @ (((((int x) ;) ((x = 1) ;)) ( (x = ((x ++) + 1)) ;)) (return x ;)) ) #symScalLoc(2) |-> 1 </store> </T>

caz în care graful de căutare corespunzător va fi: Command > show-search-graph The search graph is: Vertices:Node 8,Node 4,Node 0,Node 1,Node 10,Node 3,Node 6,Node 9,Node 7,Node 2 Edges: Rule tagged [side-effect] [Node 7,Node 9] Rule tagged [right, strict(1, 2(context(rvalue))), assign, klabel('_=_)] [Node 6,Node 8] Maude 'reduce' command [Node 0,Node 1] Unlabelled rule [Node 2,Node 3] Rule tagged [right, strict(1, 2(context(rvalue))), assign, klabel('_=_)] [Node 4,Node 7] Rule tagged [right, strict(1, 2(context(rvalue))), assign, klabel('_=_)] [Node 7,Node 10] Rule tagged [right, strict(1, 2(context(rvalue))), assign, klabel('_=_)] [Node 4,Node 6] Unlabelled rule [Node 1,Node 2] Unlabelled rule [Node 3,Node 4] dacă se dorește ieșirea din modul debug se va folosi comanda abort. Există și o variantă grafică a stepperului, în care utilizatorul are o reprezentare grafică a grafului de execuții peste care poate naviga si vizualiza configurații:

38

Comenzile din varianta grafică formează un subset al celei textuale. De notat ca unele comenzi din varianta textuală sun rezolvate implicit de varianta grafică, de exemplu comanda de vizualizare a grafului de execuții. Varianta grafică are și funcționalități suplimentare, de exemplu permite și compararea a două configurații, care ajută la analiza comportării execuției programului:

39

2.3.3 Execuţie simbolică Pentru a rula programe cu valori simbolice semantica limbajului trebuie compilată folosind opțiunea -–backend symbolic astfel: $ kompile imp.k –-backend symbolic Această opțiune are scopul de a modifica semantica limbajului astfel încât semantica originală nu este afectată, aplicându-se niște transformări prezentate în articolul [ALR13b]. Aceste transformări au scopul de a generaliza regulile de rescriere și de a facilita modul în care sunt colectate constrângerile în timpul execuției programului. Pentru programul următor: int n, sum; n = N:Int; sum = 0; while (!(n <= 0)) { sum = sum + n; n = n + -1; } rezultatul execuției simbolice va fi următorul: $ krun ../lesson_1/tests/sum.imp -cPC true <path-condition> ((notBool (N:Int <=Int 0)) ==Bool true) andBool ((notBool ((N +Int -1)

40

<=Int 0)) ==Bool false) </path-condition> <T> <k> .K </k> <state> n |-> N +Int -1 sum |-> N </state> </T> Se poate observa că acum configurația mai conține și condiția de drum asociată acestei execuții. Dacă simplificăm formula obținută vom putea trage concluzia că valoarea simbolică N este de fapt valoarea 0; cu alte cuvinte utilitarul a ’ales’ o cale de drum dintre toate cele posibile și aceasta este aceea în care valoarea variabilei n a fost considerată 0. Se mai observă în apelul krun de mai sus și faptul că sum este N, iar n este N-1, adică instrucțiunile s-au executat în același fel ca și în cazul execuției concrete atunci când n = 0. Totodată, se poate observa la apelul krun că a fost utilizată și opțiunea –cPC care este setată ca având valoarea true. Această opțiune transmite practic condiția de drum inițială, în acest caz aceasta neadăugând nici o constrângere suplimentară. Să presupunem însă că dorim să obținem toate căile de execuție posibile pentru acest program. Totuși trebuie luat în considerare faptul că datorită acelei bucle while a cărui condiție depinde de n, unde domeniul variabilei n este mulțimea (infinită) a numerelor întregi, programul are o infinitate de căi de execuție. Putem însă afla doar o submulțime finită dintre toate aceste execuții folosind opțiunea -–search pentru căutarea tuturor căilor de execuție și opțiunea –-bound pentru limitarea spațiului de căutare, astfel: $ krun ../lesson_1/tests/sum.imp -cPC -bound 3 --search Search results: Solution 1: <path-condition> (((notBool (N:Int <=Int 0)) ==Bool true) andBool ((notBool ((N +Int -1) <=Int 0)) ==Bool true)) andBool ((notBool (((N +Int -1) +Int -1) <=Int 0)) ==Bool false) </path-condition> <T> <k> .K </k> <state> n |-> (N +Int -1) +Int -1 sum |-> N +Int (N +Int -1) </state> </T> Solution 2: <path-condition> ((notBool (N:Int <=Int 0)) ==Bool true) andBool ((notBool ((N +Int -1) <=Int 0)) ==Bool false) </path-condition>

41

<T> <k> .K </k> <state> n |-> N +Int -1 sum |-> N </state> </T> Solution 3: <path-condition> (notBool (N:Int <=Int 0)) ==Bool false </path-condition> <T> <k> .K </k> <state> n |-> N sum |-> 0 </state> </T> Soluțiile afișate corespund cazurilor în care n este 0, 1, respectiv 2. Se poate observa ca valorile variabilelor sum și n sunt actualizate corespunzător. Uneori dorim să facem o analiză mai complexă a programelor, cum ar fi spre exemplu să detectăm în ce condiții o anumită instrucțiune dintr-un program se va executa. În cazul în care programul arată astfel: int n; n = read(); if (n > 0) print ”ok”; este foarte ușor de observat că instrucțiunea print ”ok”; va fi executată doar atunci când n este strict pozitiv. Însă ce se întâmplă în cazul în care programul pe care dorim să-l analizăm arată astfel:

42

Cum putem determina condițiile sub care instrucțiunea print(”error”); va fi executată? O soluție elegantă este dată de execuția simbolică care explorează toate căile de execuție și poate căuta anumite șabloane printre aceste execuții. În cazul exemplului de mai sus, folosind comanda: $ krun lists.kool --search --cIN=”#symInt(e1) #symInt(e2) #symInt(x)” --pattern=”<T> <out> error </out> B:Bag </T>” Search results: No search results putem arăta ca niciodată într-o listă ordonată adăugarea și ștergerea aceluiași element, chiar dacă acesta este duplicat, nu vor modifica conținutul listei finale. În ceea ce privește utilitatea acestei platforme de execuție simbolică, ea a fost utilizată la construirea utilitarului pentru verificarea programelor folosind logica potrivirilor denumit kcheck.

43

2.3.4 Infrastructura pentru testare Din momentul în care implementarea mediului de lucru K a devenit suficient de matură și s-au implementat/rulat diverse definiții de limbaje am creat o infrastructură de testare automată a acestora. La început testarea s-a făcut utilizând make, un utilitar prezent pe majoritatea sistemelor UNIX. Fiecare definiție K era însoțită de un fișier Makefile care preciza exact comenzile de compilare și rulare are definițiilor. În urma rulării fiecărui astfel de fișier de către vechiul sistem de testare integrată Hudson era emis un email către toți membrii proiectului dacă testarea s-a încheiat succes sau nu. După ce numărul de definiții testate a crescut și felul în care se făcea testarea a devenit insuficient (se verificau doar codurile de eroare ale utilitarelor kompile și krun) am creat un sistem care pe lângă verificarea acestor coduri testează și dacă programele s-au rulat corect (output-ul este cel așteptat). Acest sistem a fost implementat in limbajul Java și a fost făcut să funcționeze cu noua versiune a sistemului de testare integrată Jenkins. Funcționalitățile implementate au fost următoarele:

- Pornirea testării se face automat atunci când cineva a făcut o schimbare la cod în repozitoriul Subversion sau Git.

- Versiunea curentă a codului Java cu care se face testarea se actualizează automat. - Se compilează fiecare utilitar în parte și se afișează orice eroare sau avertizare la

consola Jenkins. - Fiecare definiție este compilată; sunt analizate toate erorile sau avertizările date de

către compilator și se generează un raport junit. Definițiile pot avea orice fel de opțiuni de compilare.

- Pentru fiecare definiție este generată versiunea pdf și se raportează eventualele erori. - Pentru fiecare definiție se detectează automat programele ce vor fi rulate. Utilizatorii pot

seta pentru fiecare program diverse opțiuni de rulare. Programele pot avea atașate fișiere de intrare și ieșire care vor fi folosite corespunzător pentru testarea citirii sau afișării.

- Fiecare definiție poate avea limită de timp. - Configurarea testării se face într-un fișier de configurare XML. - Rularea se face în paralel pentru definiții diferite. - Integrarea cu Jenkins utilizând rapoarte junit; pentru fiecare test este generat un tabel

într-o interfață online pentru a putea fi accesibilă de oriunde. - În cazul în care apare vreo eroare în tot procesul de testare, cel care a făcut

modificările de cod este înștiințat prin email de starea curentă. - Interfețele online sunt actualizate automat de către Jenkins în momentul în care toate

testele se încheie cu succes. Toate aceste funcționalități au fost accesibile utilizând ant la linia de comandă de către echipa de proiect. După ce am constatat că de fapt acest sistem este foarte util pentru testări locale, am decis ca el să fie pus la dispoziția utilizatorilor ca utilitar separat: ktest. Serverul Jenkins (https://fmse.info.uaic.ro/jenkins/job/k-framework-tests-git/) este notificat de către GitHub (https://github.com/kframework/k) ori de câte ori codul framework-ului K este modificat. Această notificare pornește actualizarea codului sursă de pe GitHub și îl compilează

44

cu javac prin intermediul ant. După compilare este rulat ktest peste un fișier de configurare care include toate definițiile curente. Dacă testarea s-a încheiat cu succes atunci interfața online (https://fmse.info.uaic.ro/tools/K/) este actualizată automat. Utilizarea ktest

ktest este un utilitar disponibil la linia de comandă care primește la intrare un fișier de configurare sau o definiție de limbaj și testează automat toate definițiile din acel fișier, respectiv definiția dată ca argument. Fișierul de configurare conține o colecție de teste de forma: <test            definition="tests/regression/subsort-­‐klabel/issue.k"            programs="tests/regression/subsort-­‐klabel/programs"            results="tests/regression/subsort-­‐klabel/tests"            extension="issue"  >            <all-­‐programs>                <krun-­‐option  name="-­‐output"  value="none"  />                <krun-­‐option  name="-­‐color"  value="off"  />            </all-­‐programs>            <program  name="test.issue">                <krun-­‐option  name="-­‐output"  value="pretty"  />            </program>    </test> Fiecare test are atașată o definiție, unul sau mai multe directoare de programe, unul sau mai multe directoare de rezultate pentru testarea intrărilor/ieșirilor, diverse opțiuni pentru programe setate la nivel global sau local, extensiile fișierelor ce conțin programele, incluziuni de alte fișiere de configurare. Opțiunile ktest sunt următoarele: $ ktest --help usage: ktest <file> [options] <file> is either a K definition (single job mode) or an XML configuration (batch mode). -h,--help Print this help message. --version Print version information. -v,--verbose Verbose output. --color <[on|off|extended]> Use colors in output. (Default: on) --programs <dir> Programs directory in single job mode, or a root directory for programs in batch mode. By default this is the directory where <file> reside. --extensions <string> The list of program extensions separated by whitespaces. Required in single job mode, invalid in batch mode. --exclude <file> The list of programs which will not be tested. Valid only in single job mode. --results <dir> Directory containing input and

45

expected output for programs in single job mode, or a root directory for the expected I/O for programs in batch mode. By default this is the directory where <file> reside. --skip <steps> The list of steps to be skipped, separated by whitespace. A step is either [kompile|pdf|krun]. -d,--directory <dir> A root directory where K definitions reside. By default this is the current directory. Valid only in batch mode. --report Generate a junit-like report. --timeout <num> Time limit for each process (milliseconds). Default is 300000 milliseconds. --ignore-white-spaces <on|off> Ignore white spaces when comparing results. (Default: on). --ignore-balanced-parentheses <on|off> Ignore balanced parentheses when comparing results. (Default: on). --dry Dry run: print out the command to be executed without actual execution. Aceste opțiuni sunt active în funcție de modul de utilizare al ktest. Dacă se dorește testarea obișnuită, utilizând un fișier de configurare utilitarul se rulează cu următoarele opțiuni: $ ktest config.xml --programs root1 --results root2 Fișierul config.xml conține descrierea testelor, root1 reprezintă directorul care conține programele, iar root2 conține rezultatele. Atunci când se dorește testarea unei singure definiții, ktest poate infera din opțiuni întreaga configurație de testare: $ ktest definition.k --programs root1 --results root2 --extensions “def1 def2” –-exclude “pgm1 pgm2” Folosind parametrii dați ca argument ktest construiește automat o configurație internă și o rulează ca pe una obișnuită. Opțiunile –extensions și –exclude au sens doar atunci când sunt utilizate pentru testarea unei singure definiții, pe când –programs și –results pot fi utilizate în ambele cazuri prezentate mai sus. Semantica fiecărei opțiuni este prezentată mai jos:

● --programs : specifică directorul rădăcină al programelor. Toate căile din fișierul de configurare sunt relative la acest director. În cazul testării unei singure definiții se pot acest folder reprezintă directorul rădăcina al programelor.

● –-results: specifică directorul rădăcină al locațiilor ce conțin fișiere de input sau de output. Toate căile din fișierul de configurare sunt relative la acest director. În cazul testării unei singure definiții se pot acest folder reprezintă directorul rădăcina unde se găsesc rezultatele programelor.

● –-extensions: specifică o listă de extensii de programe care este folosită pentru

46

detectarea automată a acestora într-un director specificat. ● –-exclude: specifică o listă de programe care sunt vor excluse din testare. ● –-skip: inhibă anumiți pași de testare: compilarea, generarea de fișiere pdf sau

testarea programelor ● –d, --directory: specifică directorul rădăcină unde se află definițiile K. Această

opțiune este activă doar atunci când se utilizează fișiere de configurare. Valoarea implicită este directorul curent.

● –-color: specifică dacă testele folosesc culorile la afișare și dacă se vor folosi coduri de culoare care nu sunt ASCII.

● -–report: generează rapoarte JUnit. ● --timeout: setează timpul maxim de execuție per proces. ● –-ignore-white-spaces: specifică dacă la compararea ieșirilor proceselor asociate

programelor cu ieșirile așteptate sunt ignorate spațiile. ● –-ignore-balanced-parantheses: specifică dacă la compararea ieșirilor

proceselor asociate programelor cu ieșirile așteptate sunt ignorate parantezele. ● --dry: generează comenzile interne de rulare. Această opțiune este utilă la construirea

corectă a fișierelor de configurare. ● --verbose: afișează informații suplimentare referitoare la starea actuală a unui proces

la momentul rulării. Se pot observa ușor care procese s-au încheiat, ce programe s-au terminat de executat și timpii de execuție.

2.4. Logica Potrivirilor (Matching Logic) Logica potrivirilor a fost introdusă de Roșu et al. [RS09, RES09] ca un mecanism de verificare a programelor independent de limbaj inspirat din logica rescrierilor. Inițial [RS09], logica potrivirilor a fost gândită ca un mecanism de a da o semantică axiomatică pentru limbaje de programare, semantică de la care se poate construi un verificator de programe. Logica potrivirilor se bazează pe noțiunea de pattern, care constă dintr-o configurație abstractă (cu variabile) și o formulă logică de ordinul I care constrânge variabilele din configurația abstractă. Configurațiile concrete sunt satisfăcute de un pattern dacă configurația concretă este o instanță a configurației abstracte din pattern și în plus toate constrângerile de ordinul I sunt satisfăcute. De exemplu, configurația concretă

se potrivește cu (este satisfăcută de) pattern-ul:

dând variabilei a valoarea 3 (număr natural) și variabilei ρ valoarea z |-> 5 (un map). Constrângerea din celula form (a >= 0) este satisfăcută de această asignare a variabilelor (a = 3). Avantajul logicii potrivirilor in comparație cu logicile de tipul Floyd/Hoare este că structura configurației nu este pierdută și poate fi folosită în procesul de verificare pentru a simplifica

47

substanțial formulele care apar. De asemenea, este mai intuitivă, deoarece, spre deosebire de logica Hoare, regulile sunt de tip “forward” și nu introduc cuantificatori:

Regula pentru asignare în logica Hoare:

Regula pentru asignare în logica Floyd:

Regula pentru asignare în logica potrivirilor: In plus, logica potrivirilor face ca regula de demonstrație pentru bucle while:

să fie mai puternică decât regula corespunzătoare din logica Floyd/Hoare:

deoarece este validă chiar dacă expresia booleană e din condiția buclei conține efecte secundare (cum ar fi incrementări de variabile (x++)). Mai mult, structurile de date cum ar fi listele sau arborii pot fi axiomatizate prin echivalențe de configurații, ceea ce permite raționamentul asupra heap-ului într-un mod similar cu logica separării. De exemplu, axioma de mai jos:

axiomatizează listele ca termeni list(p, α). Termenul lisp(p,α) denotă o listă α ce apare în heap la poziția p. În mod natural, list(p, α) este axiomatizat printr-o disjuncție: sau p este 0 (nil) și α este vidă, sau p este o locație ce conține primul element a al listei și pointerul q spre restul listei și list(q, β) este lista ce începe la q iar α este formată din a urmata de β. Axioma de mai sus poate fi folosită pentru a arăta implicațiile:

și

iar aceste din urmă configurații pot fi referite prin pattern matching. În [RS11a], este descris modul în care logica potrivirilor poate fi obținută direct din semantica operațională a limbajului de programare în care sunt scrise programele de verificat. Astfel, încrederea că demonstrația obținută este corectă crește, deoarece semantica operațională, spre deosebire de semanticile axiomatice clasice, este executabilă și poate fi testată. În plus, în același articol este prezentată o implementare prototip a unei unelte bazată pe logica potrivirilor și care poate verifica programe scrise într-un limbaj C minimal denumit KernelC. Limbajul

48

KernelC a fost definit in K, iar verificatorul de programe (denumit MatchC) este bazat pe aceasta semantica. Verificatorul poate verifica programe care tratează structuri de date cum ar fi listele:

și poate demonstra că anumite proceduri care manipulează astfel de structuri sunt corecte. Spre exemplu, procedura următoare inversează o listă simplu înlănțuită:

Procedura este prevăzută cu adnotări (invarianți, precondiții și postcondiții) scrise în logica potrivirilor. Verificatorul MatchC (bazat pe Maude) verifică că aceste adnotări sunt corecte și că, în consecință, procedura respectă specificațiile. În cadrul proiectul DAK, logica potrivirilor s-a dezvoltat semnificativ, după cum se va descrie mai jos. Primul pas în dezvoltarea logicii potrivirilor în cadrul proiectului a fost reprezentat de punerea unor baze teoretice puternice. În [RS11b,RS12b] se abordează problema obținerii exacte a unei semantici axiomatice pornind de la semantica operațională, dată ca reguli de rescriere de forma:

Este bine cunoscut faptul că astfel de reguli de rescriere pot fi folosite pentru a defini (operațional) orice limbaj de programare. Din păcate, astfel de semantici operaționale nu sunt considerate potrivite pentru a raționa despre programe deoarece demonstrațiile sunt de nivel jos, se bazează de cele mai multe ori pe inducția după numărul de pași și se lucrează direct cu sistemul de tranziții generat. Pe de altă parte, semanticile axiomatice (pentru logica Hoare) sunt bine echipate pentru raționamentul despre programe, dar sunt greu de testat și trebuie demonstrat că ele sunt echivalente cu o semantica operațională de referință. Abordarea din [RS11b,RS12b] propune un prim sistem deductiv (sistem de demonstrație) pentru logica potrivirilor care este independent de limbaj. Altfel spus, sistemul deductiv primește la intrare limbajul de programare (sau semantica operațională a limbajului de programare) și produce perechi de pattern-uri din logica potrivirilor de forma:

49

cu semnificația că orice configurație concretă care se potrivește peste φ se poate rescrie într-o configurație concretă care se potrivește peste φ’. Astfel de perechi de pattern-uri generalizează triplete Hoare:

prin faptul că atât partea dreaptă cât și partea stângă conțin structura completă a configurației, inclusiv partea de cod. Sistemul de demonstrație propus este alcătuit din nouă reguli, grupate în funcție de scop. Primele patru reguli sunt de natură operațională:

și permit transformarea semanticii operaționale A în perechi de pattern-uri φ � φ’ valide. Următorul set de reguli sunt deductive și permit raționamentul propriu-zis:

În fine, ultima regula, Circularitatea:

este regula cea mai importantă prin faptul că permite verificarea invarianților pentru construcții repetitive într-un mod independent de limbaj. Spre exemplu, regula de circularitate poate fi folosită atât pentru a demonstra bucle while, cât și funcții recursive sau salturi (jump-uri, goto-uri). Principalele atuuri ale acestui sistem deductiv format din nouă reguli sunt independența de limbaj și faptul că se bazează pe o semantică operațională. Astfel, deoarece pentru verificare nu intervine o semantică axiomatică în plus, nivelul de încredere în demonstrațiile făcute este mai ridicat. Deoarece sistemul deductiv este independent de limbaj, el este demonstrat a fi corect o singură dată (spre deosebire de abordările de tip Hoare, unde pentru fiecare limbaj, semantica axiomatică trebuie demonstrată a fi corectă în raport cu semantica operațională). În plus,

50

MatchC poate fi văzut ca o implementare a acestui sistem deductiv.

2.5. Utilitar pentru Logica Potrivirilor Utilitarul care implementează verificarea programelor utilizând logica potrivirilor este construit peste platforma de execuție simbolică prezentată în [ALR13b]. Acesta poartă denumirea de kcheck și primește la intrare atât semantica unui limbaj de programare (dată utilizând reguli de rescriere) cât și un set de formule care urmează a fi verificate. Programele sunt caracterizate în general de o singură formulă de forma π ∧ ϕ ⇒ π′ ∧ ϕ′ dar de cele mai multe ori pentru a demonstra această formulă este nevoie de mai multe formule ajutătoare care ajută la demonstrație atunci când se aplică deducția [Circularity] din sistemul deductiv al logicii potrivirilor. kcheck aplică sistemul deductiv al logicii potrivirilor folosind un alt sistem deductiv modificat al execuției simbolice dar care este echivalent cu primul, așa cum este arătat în raportul [ALR13b]. Motivația utilizării altui sistem deductiv este dată de faptul ca cel de-al doilea sistem deductiv are avantajul unei implementări mai ușor de efectuat și mai modular din punct de vedere al ingineriei programării. Totodată, această abordare ne-a permis și o separare a motorului de execuție simbolică de partea de verificare, acest motor fiind primul motor de execuție generic în ceea ce privește limbajul de programare, bazat pe semantica limbajelor. Publicația [ALR13b] reflectă atât importanța unui motor de execuție generic (acceptat de comunitatea internațională) cât și faptul că întregul framework K care a fost dezvoltat în acest proiect poate fi utilizat și în acest scop.

51

Descriere generală Modul de funcționare a kcheck este detaliat în această subsecțiune. Fiecare formulă π ∧ ϕ ⇒π′ ∧ ϕ′ atașată unui program P are următoarea semnificație: dacă programul satisface precondiția π ∧ ϕ atunci, după execuția sa, acel program satisface postcondiția π′ ∧ ϕ′ . La momentul verificării, kcheck utilizează motorul de execuție de simbolică astfel:

- asumă π ca fiind configurația inițială și ϕ ca fiind condiția de drum inițială; - execută simbolic configurația inițială și acumulează constrângerile date de semantica

limbajului de programare. După finalizarea execuției simbolice, configurația finală π′′ trebuie sa conțină programul vid (echivalentul execuției cu success a programului) și o formulă logică în condiția de drum acumulată ϕ′′. Pentru a finaliza verificarea programului P utilitarul kcheck face apel la SMT solver-ul Z3 pentru a rezolva implicația π′′ ∧ ϕ′′ → π′ ∧ ϕ′. Această implicație verifică efectiv dacă configurația finală la care s-a ajuns folosind execuție simbolică este conformă cu postcondiția π′ ∧ ϕ′ a programului P. În mod evident, execuția simbolică poate returna mai multe configurații finale π′′ ∧ ϕ′′ corespunzătoare tuturor căilor de execuție ale programului P. În cazul în care programul are o mulțime infinită de căi de execuție acestea se pot limita, folosind mărginirea spațiului de căutare al căilor de execuție. kcheck investighează fiecare configurație π′′ ∧ ϕ′′obținută și verifică toate implicațiile posibile utilizând SMT solverul. Dacă una dintre aceste implicații nu are loc, atunci formula nu poate fi demonstrată, deoarece există cel puțin o cale de execuție în programul P care violează proprietatea π′ ∧ ϕ′. Pe de altă parte, folosirea logicii potrivirilor pentru verificare are particularitatea că pot fi utilizate reguli ajutătoare pentru demonstrare. Cu alte cuvinte, pentru a evita explozia spațiului căilor de execuție determinate de obicei de bucle sau salturi înapoi în programe pot fi folosite așa numitele circularități. Acestea sunt formule din logica potrivirilor care corespund unor bucăți de program și care pot fi utilizate de către kcheck la momentul execuției simbolice. O particularitate a unei astfel de formule este că poate fi utilizată la propria demonstrație. Conform principiului circularității [RL09], o mulțime de formule se demonstrează într-un mod monolitic: dacă procesul de demonstrare se termină cu succes, atunci toate formulele au loc. Dacă demonstrarea uneia dintre formule eșuează, atunci nu putem trage nici o concluzie despre niciuna dintre formule. De exemplu, dacă vom considera cazul unei bucle de forma while  B  do  S pentru care precondiția este ϕ și postcondiția este ϕ′ atunci kcheck va analiza următoarele cazuri:

- B nu are loc și bucla nu se poate executa; în acest caz condiția obținută în urma execuției este ¬B ∧ ϕ

- B are loc și bucla se poate executa; în acest caz, se va executa S cu precondiția B ∧ ϕ și în urma execuției se obține B ∧ ϕ ∧ ϕ!, unde ϕ! este condiția de drum acumulată. kcheck verifică dacă această formulă obținută implică poscondiția buclei ϕ′. La ce-a doua iterație a buclei, formula demonstrată la prima iterație poate fi refolosită direct, conform sistemului deductiv al logicii potrivirilor (vezi regula de circularitate). Prin urmare, kcheck demonstrează direct proprietăți ale buclelor de program, fără a executa

52

simbolic bucla decât o singură dată. Astfel, este evitat cazul în care execuția simbolică poate avea o durată de timp infinită. Utilizare kcheck kcheck este un utilitar disponibil în linia de comandă, funcționabil sub platformele Linux și Mac OS X. Opțiunile acestui utilitar (cât și felul în care pot fi vizualizate) sunt prezentate mai jos: $ kcheck --help usage: help [-d <arg>] [-h | -v] [-p <arg>] [-prove <arg>] [-simplify] Compiles the K definitions given as arguments. -d,--definition <arg> main file to kompile -h,--help prints this message and exits -p,--pgm <arg> program file used to build the initial configuration -prove <arg> file containing reachability rules -simplify simplify the path condition before sending it to SMT solver -v,--verbose verbose mode Opțiunea --help afișează toate opțiunile kcheck. Opțiunea --definition <arg> primește un fișier .k care conține semantica K a unui limbaj de programare. Această opțiune este folosită împreună cu opțiunea -prove <arg> care conține formulele din logica potrivirilor ce trebuie demonstrate, date utilizând sintaxa K. Verificarea unui fișier cu formule se face cu un apel de forma: $ kcheck definition.k -prove formulas.k Celelalte opțiuni sunt suplimentare:

● --simplify activează un simplificator de formule scris în K care are scopul de a optimiza dimensiunea formulei ce urmează a fi trimisă la SMT solver.

● -p, --pgm <arg> primește la intrare un program care este folosit pentru a inițializa configurația atunci când aceasta este foarte mare. Această opțiune este utilizată pentru abstractizarea formulelor, concretizarea urmând să fie făcută dinamic prin execuția programului dat ca argument și îmbinarea cu partea stângă a formulei de demonstrat.

● -v, --verbose afișează informații suplimentare referitoare la încheierea etapelor (construcția configurației inițiale, execuția simbolică, verificarea implicațiilor)

Rezultatele afișate de kcheck sunt configurațiile programelor verificate. Dacă vreuna dintre acestea nu conține configurații finale (celula <k> nu este vidă) atunci verificarea a eșuat. În cazul în care toate configurațiile afișate sunt finale se poate trage concluzia ca verificarea a avut loc succes.

53

2.6. Limbaje de programare implementate în K Framework

2.6.1. Object Constraint Language (OCL) Limbajul OCL este un limbaj de constrângeri peste diagrame UML, utilizat în ingineria software. Semantica acestui limbaj a fost o provocare pentru mediul de lucru K deoarece el necesită un limbaj de modelare suport peste care să fie rulate diversele constrângeri exprimate folosind OCL. Spre exemplu, constrângerile: context Meeting inv: if start < end then self.participants->size() >= 2 else false endif context TeamMeeting inv: self.participants->iterate(participant ; major : true | major and participant.age > 0) au sens doar în condițiile în care există un model UML care descrie clasele TeamMeeting și Meeting cu toate câmpurile și metodele. Cu ajutorul acestor tip de constrângeri se pot exprima proprietăți de invarianță ale claselor, precondiții și postcondiții pentru metodele acestora care au loc într-un context clar specificat. Semantica K a limbajului OCL a fost prezentată în articolul [LR11]. Implementarea acesteia se găsește la adresa: https://github.com/kframework/modelink . Sintaxă Principalele funcționalități implementate în această semantică sunt conforme cu standardul OCL 2.3 publicat de Object Management Group (OMG). Sintaxa OCL include sintaxa expresiilor OCL, enumerațiile, referințe la obiecte, câmpuri și metode (statice și non-statice), tipurile de bază ale OCL și colecții. De remarcat aici sunt expresiile OCL care nu sunt tipizate (conform standardului) și care includ atât expresii uzuale peste tipurile de bază (numere întregi, șiruri de caractere, numere reale, valori booleene) cât și expresii care iterează peste colecții. Implementarea conține și sintaxa pentru modele și metamodele UML (declarații de clase, câmpuri și metode, referințe, enumerații, declarații de instanțe ale claselor). Semantică Configurația semanticii K a OCL are 45 de celule, dintre care 34 stochează informații despre modelul curent și metamodelul din care face parte, iar restul de 11 celule păstrează informații despre constrângerea curentă care urmează să fie verificată (contextul curent, starea variabilelor, etc.). În ceea ce privește regulile de rescriere, implementarea include 74 de reguli ce reprezintă strict semantica OCL și 18 reguli de rescriere care încarcă modelul și metamodelul. Semantica implementează următoarele funcționalități ale OCL:

54

· Verificarea invarianților de clasă peste instanțele unui model · Suport pentru referința la contextul curent: self · Suport pentru operații peste numere întregi: +,-,*, / · Suport pentru operații booleene: <=, >=, <, >, <>, =, and, or, xor, not, implies · Suport pentru let-expresii: let_in_ · Suport pentru operații peste colecții: forAll, exists, size, iterate · Suport pentru moștenire simplă și multiplă · Suport pentru verificarea precondițiilor și postcondițiilor

Semantica a fost utilizată și pentru execuția de scenarii, în vederea verificării dinamice a constrângerilor OCL. Un exemplu de astfel de scenariu este următorul: scenario meet { kmeeting.confirm(); kmeeting.confirm(); } Metoda confirm() este specificată astfel: context Meeting::confirm() pre: isConfirmed = false post: isConfirmed = true Se poate observa ca o dată confirmată o întâlnire, aceasta nu mai poate fi confirmată încă o dată deoarece precondiția nu mai este satisfăcută la cel de-al doilea apel. Practic, utilizând semantica putem executa cu framework-ul K direct specificația OCL a unei metode, fără a cunoaște codul sursă al acesteia. Această semantică a limbajului OCL a necesitat îmbinarea mai multor limbaje (limbaj pentru scrierea meta-modelelor UML, limbaj pentru scrierea modelelor, limbaj pentru constrângerile OCL) solicitând capacitățile de parsare ale K-ului. Prin implementarea acesteia, am arătat ca această îmbinare de limbaje este posibilă și am oferit totodată și un exemplu pentru cei care doresc să combine diverse limbaje atunci când utilizează K.

2.6.2. Java Semantica limbajului Java este una dintre cele mai complexe semantici de limbaj

dezvoltate in K Framework. Scopul proiectului este o semantica completa si executabila a limbajului, testata riguros pe o suita cuprinzătoare de teste. O astfel de semantica ar servi mai multor scopuri. In primul rând, este o demonstrație a utilității K Framework pentru a defini semantici complexe a limbajelor moderne. In al 2-lea rând, aceasta semantica urmează să fie utilizată pentru analiza de programe utilizând tool-uri din K independente de limbaj. In al 3-lea rând, testele și interpretoarele dezvoltate pot să-și găsească utilitatea în alte proiecte.

Dezvoltarea a urmat specificația oficiala Java , așa cum este descrisă în Java Language Specification ediția 2 (JLS) [GJS00]. Proiectul a început încă în martie 2012, în K versiunea 2. Pe măsura ce noua versiune s-a maturizat s-a făcut tranziția la K versiunea 3. Totodată

55

semantica a început să utilizeze unele facilități noi de K, cum ar fi căutarea peste spațiul de soluții, o mai buna gestionare a priorităților operatorilor și altele.

Toate caracteristicile limbajului Java sunt complet implementate - operatori , instrucțiuni , metode , clase cu toate categoriile de membri , moduri de acces , supraîncărcare , package-uri , clase interne și locale și multi-threading . Dimensiunea semanticii poate fi exprimate prin următoarele metrici. Dimensiunea codului sursă este de 191 KB , fără comentarii , conține 869 de reguli și peste 200 de construcții sintactice auxiliare. Toate caracteristicile au fost testate temeinic executând mici programe sau prin model checking .

Deși K Framework suportă definirea unei gramatici pentru limbaj, semantica Java se bazează pe o gramatică definită în SDF[HHK89]. Acest lucru sa întâmplat în primul rând pentru că o gramatică SDF pentru Java era deja disponibilă când a fost demarat proiectul semantica Java . Decizia avea sens – mai degrabă reutilizăm resursele existente decât să dezvolte o nouă gramatică în alt format, pornind de la zero. În al doilea rând , la acel moment capabilitățile de definire ale sintazei pentru K erau limitate. Primind la intrare o gramatică SDF, un generator de parsere independent de limbaj compilează acest gramatică într-un parser . Acest parser este ulterior folosit pentru a parsa programele Java în formatul acceptat de către K la intrare. Deoarece gramatica este definită extern , K nu are acces la gramatică. Ca urmare , semantica trebuie să fie definită pe reprezentarea AST (Abstract Syntax Tree – arbori sintactici abstracți) [JJ03] a programelor , mai degrabă decât direct pe reprezentarea lor sintactică .

Proiectul a fost dezvoltat folosind metodologia Test Driven Development – dezvoltare bazată pe teste. Înainte ca fiecare caracteristică de limbă majoră să fie dezvoltată, procedam la identificarea aspectelor care trebuie să fie testate . Pe baza acestor aspecte se elabora un plan de testare, și pe baza planului de testare - lista de teste. Numai atunci când testele erau gata și puteau fi executate cu JDK (Java Development Kit – implementarea oficiala a Java de la Oracle), extinderea efectivă a semanticii era implementată. Cu toate acestea, procesul nu era bătut în cuie. De multe ori in timpul dezvoltării ne-am dat seama că testele existente sunt insuficiente pentru a testa toate cazurile - atunci noi teste erau adăugate la nevoie. În acest fel am produs o semantică de o înaltă calitate, una care are toate cazurile marginale implementate și testate. Putem spune cu încredere că actuala semantică este completă. Suita de teste întreagă conține peste 800 de teste . Să dezvoltăm semantica în acest fel a avut perfect sens. Am avut o specificație clară de la început – documentul JLS, o specificație care nu se schimba de la o zi la alta. Testele sunt programe Java scurte. Acestea nu au nevoie de un context complex pentru a fi executate – se execută de la linia de comandă. Putem spune că un proiect de semantică limbaj bazat pe o specificație este tipul potrivit de proiect pentru Test Driven Development[B03]. Un produs secundar al proiectului este suita de teste, care poate fi utilizată în alte proiecte ce țin de limbajul Java.

In unul dintre referatele de doctorat anterior a fost comparată semantica prezentă cu alte proiecte ce reprezentau o semantică Java. La acel moment semantica prezentă avea doar un singur tip de clase interne implementat și nu avea suport pentru multithreading. Semantica K-Java a fost comparată cu proiecte Jitan[ACR98], Java – FAN[FCM04] și Jbook[SBS01]. Proiectul JITAN nu a putut fi testat pentru că nu aveam acces la codul lui sursă. Celelalte două proiecte au fost testate și au picat o parte semnificativă din testele scrise pentru K-Java. În timp ce aceste proiecte afirmau că au implementat cele mai multe caracteristici ale Java, de fapt, caracteristicile limbajului au fost doar "ilustrate". Acele semantici executau corect cazurile

56

principale, însă cazurile marginale adesea nu erau suportate. Ceva mai târziu am rulat actuala semantică peste setul de exemple distribuite cu JBook și Java-Precisely și am constatat că toate exemplele de programe care ar putea fi utilizate ca teste de limbaj au fost executate cu succes de prezenta semantică.

La testarea semanticii, unele aspecte nu au putut fi testate de prin simplă execuție. Un exemplu bun este multi-threading-ul. Pentru aceasta am folosit capabilități de model-checking ale K Framework. Inițial am marcat toate regulile din semantică ca și tranziții. Aceasta a dus la o explozie a spațiului de stări dincolo de capabilitățile oricărui sistem de calcul. A fost nevoie de a limita tranzițiile la doar câteva reguli, cele direct legate de threading, citire/scriere variabile și tipărire la ieșirea standard. În continuare am proiectat un set de teste care exploatează diferite capabilități ale multi-threading-ului - creare thread, join, sincronizare și metodele wait/notify. Fiecare din aceste teste a fost utilizat pentru model-checking, pentru a colecta toate rezultatele posibile pe toate căile de execuție posibile. Ieșirile au fost apoi comparate cu setul așteptat de ieșiri, și astfel a fost certificată corectitudinea facilității de multi-threading.

Un alt aspect al semanticii care a fost testat prin model-checking a fost determinismul. În K Framework diferența dintre evaluarea argumentele unui operator în orice ordine, comparativ cu evaluarea acestora într-o anumită ordine este marcat de un singur cuvânt cheie. Astfel, este foarte ușor de a comite o eroare aici, prin utilizarea cuvântului cheie nepotrivit. Execuția simplă nu va dezvălui eroarea în acest caz. Pentru un anumit program cu o anumită intrare regulile de ordine ale semanticii vor fi întotdeauna aplicate în aceeași ordine. În Java toate expresiile sunt evaluate determinist stânga la dreapta. Astfel, este posibil să avem o semantică teoretic incorectă care totuși produce un interpretator corect. Pentru a testa acest gen de erori am utilizat model-checking. Totuși, această abordare a fost folosită în doar câteva locuri, este nevoie de mai multe teste pentru ne asigura că semantica nu prezintă nedeterminism nedorit.

În cele din urmă , am încercat să folosim semantica noastră cu noile instrumente de execuție simbolice pentru K Framework. Când s-a executat simbolic un program care constă doar din variabile simple, s-au obținut rezultatele așteptate. Însă programele care utilizează tablouri și polimorfism cu valori simbolice nu sunt încă suportate. Această facilitate abia urmează să fie implementată.

In continuare va fi prezentata arhitectura in linii mari a semanticii – configurația, etapele de preprocesare si rolul fiecărei celule.

57

Configurația este împărțit în trei grupuri de celule mari. Grupul <threads> conține una sau mai multe celule <thread>. Aici sunt păstrate datele legate de execuția unui thread, cum ar fi computația, stivă, mediul local de variabile. Al doilea grup este înglobat în <classes> care conține mai multe celule <class>. Acestea includ toate informațiile legate de fiecare clasă in parte. Celulele rămase sunt celulele de nivel superior - cel de-al treilea grup. Celulele de nivel superior țin de reprezentarea memoriei, datele globale necesare pentru sincronizarea thread-urilor și celule auxiliare utilizate pentru depanare.

Unele celule din configurație nu sunt utilizate de către reguli. Acestea servesc doar pentru gruparea alte celule după context. Celulele non-semantice utilizate pentru grupare sunt galbene. Celulele de alte culori sunt celule semantice propriu-zise.

În timpul fazei de preprocesare există o singură celulă <thread>. Această celulă servește pentru a păstra computația în toate fazele de preprocesare, pentru întregul program. În timpul fazei de execuție însă pot exista mai multe celule <thread> - câte una pentru fiecare fir de execuție. În <thread>sunt conținute celulele frunză <stack> și <k>, și celulele containere <methodContext> și <threadData>.Celula <k> conține computația curentă, atât în fazele de preprocesare cât și în cea de execuție. Atunci când celula <k> rămâne goală acest lucru semnalizează sfârșitul fazei de preprocesare curente și tranziția la faza următoare. Atunci când celula <k> rămâne goală în timpul fazei de execuție, execuția thread-ului curent se încheie. Următoarea celulă din <thread>, celula <stack> reprezintă stiva thread-ului.

În interiorul celulei <methodContext> sunt diverse date ce țin de contextul metodei curent executate. Aici avem:

58

· <env> cu valori de tip Map[Id->Int] - un map cu chei reprezentând variabile locale si valori reprezentând adresa de memorie în celula <store>. · <localClassesEnv> ține de clasele locale și va fi explicată mai jos. · <return> - tipul returnat de metodă. · <contextType> - poate avea una din două valori: staticCT sau instanceCT, în funcție de proprietatea metodei curente de a fi statică sau non-statică. · <crntObj> - obiectul asociat cu metoda curentă, dacă există așa un obiect. În context non-static <crntClass> conține clasa în care această metodă este definită, iar <location> conține locația obiectului curent în <store>. Dacă contextul este static atunci celule au valori goale.

Grupul de celule <threadData> conține: · <tid>:Int - id-ului subiectului. · <holds>:Map[Int -> Int] - un map de la locații de obiecte la numere întregi. Cheile sunt obiecte monitor pe care thread-ul curent deține un lock. Valorile reprezintă de câte ori lock-ul a fost ocupat de către thread. · <interrupted>:Bool - valoare boolean care semnalizează dacă thread-ul curent a fost întrerupt.

Din punctul de vedere al evaluării, semantica este împărțită în mai multe etape de preprocesare a programului, urmate de execuția propriu-zisă. Fazele de preprocesare sunt aproximativ echivalente cu compilarea unui program java. Preprocesările realizează toate computațiile care sunt tradițional implementate în compilator. Mai jos este lista tuturor fazelor de evaluare: · Procesare Nume Tipuri · Procesare Unități Compilare · Procesare Declarații Clase · Procesare Membri Clase · Elaborare · Execuție

Etapa curentă de evaluare a semanticii este stocată în <globalPhase>. Celula este inițializată cu id-ul primei etape - ProcTypeNamesPhase.

Urmează celulele din grupul <phStart>, care există de la începutul programului: · <program> - Programul de intrare, în format AST (Abstract Syntax Tree). · <mainClass>:String - Clasa de pornire, cea care conține metoda main().

Ambele celule sunt inițializate pe baza argumentelor primite din linia de comandă, la fel cum este cazul și în JDK Java.

Celulele globale rămase sunt grupate în funcție de faza în care intră în rol pentru prima oară. Astfel, celulele din <phTN> sunt populate în timpul fazei Procesare Nume Tipuri, celulele din <phCU> - în timpul Procesare Unități Compilare și așa mai departe. Ultimul grup de celule globale, <groupDebug>, servesc doar pentru depanare.

În faza Procesare Nume Tipuri semantica trece prin toate unitățile de compilare și calculează două celule globale:

59

· <namesToClasses> de tip Map[PackageId -> Map[Id -> ClassType]]. Un map pe două nivele. Primul nivel este o hartă de la nume de package-uri la o altă hartă. Harta de pe nivelul 2 este de la nume simple de clasă într-un package la nume de clasă complete (complet calificate, fully qualified class names conform JLS). Adică nume de clasă precedate de numele complet al package-ului în care sunt definite. Această celulă este utilizată pe larg în semantică. Map-ul conține atât clase de nivel superior cât și clase interne. Pentru clasele interne package-ul este numele complet calificat al clasei ce le include (enclosing class). · <classesToAccessModes> : Map[ClassType -> AccessMode] - Map de la nume de clasă la moduri de acces, pentru toate clasele.

Faza Procesare Unități Compilare primește din nou la intrare întregul program și îl analizează la un nivel mai profund. Datele colectate în etapa anterioară sunt utilizate pentru a procesa clauzele imports ale unităților de compilare. Temporar, aceste date sunt stocate în celula: · <compUnitImports>:Map[Id -> ClassType] - un map de la nume de tip accesibile în această unitate compilare la numele complet calificat al claselor. Acestea includ atât clase accesibile prin declarații imports cât și clase declarate în același package cu unitatea de compilare curentă.

În continuare tot în această fază fiecare clasă este stocată într-o celulă <class>. Din nou, sunt parcurse atât clasele de nivel superior cât și cele interne sunt. Într-o celulă <class> proaspăt creată doar câteva celule sunt populate cu date. Dintre acestea, trei au un rol central în toată semantica: · <className> - Numele complet calificat al clasei. · <metaType> - Ne spune dacă tipul salvat în această celulă este clasă sau interfață. Pentru a evita terminologia de prisos, ne vom referi de acum înainte atât la clase cât și la interfețe cu termenul "clase", făcând distincție doar atunci când este necesar. · <classPhase> - reprezintă starea clasei curente. În afară de etapa de evaluare globală fiecare clasă se poate afla și ea în una din câteva etape. Fazele pentru clase sunt necesare pentru a ține evidența care clase au fost procesate în etapa globală curentă și care nu. În fiecare etapă globală toate clasele trebuie să tranziționeze către o anumită fază clasă. Cu toate acestea, relația între etapele globale și fazele clasă nu este de unu la unu. În unele faze globale se pot întâmpla mai multe tranziții per-clasă, în altele - nici una. Ordinea în care sunt procesate clasele este în general impusă de relația de dependență între clase.

Fazele pentru clase sunt: · Creat - faza inițială. La sfârșitul etapei Procesare Unități Compilare toate clasele sunt în faza "Creat". · Baze procesate · Declarații procesate · Membri procesați

În plus față de cele trei celule de mai sus, în timpul etapei Procesare Unități Compilare mau sunt salvate câteva celule. Acestea sunt grupate în celula <cphCreated>:

60

· <enclosingClass> - clasa care include claca curentă, dacă clasa curentă este internă. · <rawExtends> - clauza extends a clasei curente, în forma inițială. · <rawImplements> - clauza implements în forma inițială. · <rawDeclarations> - Corpul clasei în forma AST inițială. · <cuImports> : Map[Id -> ClassType] - Pentru clasele de nivel superior, această celulă copie celula <compUnitImports> calculată în cadrul unității de compilare curente. Pentru clasele interne celula este goală. Clasele din această celulă sunt necesare pentru a rezolva clauzele extends/implements ale claselor de nivel superior.

După cum putem vedea, celulele salvate în timpul fazei clasă Creat conțin toate datele din AST-ul original al clasei. Astfel, reprezentarea inițială a programului ca și AST nu mai este necesară. De fapt, celula <program> este ștearsă la sfârșitul etapei Procesare Unități Compilare. Etapele de preprocesare rămase vor folosi datele clasei în această formă inițială pentru a calcula alte celule din <class>, folosite în cele din urmă pentru execuție.

Următoarea fază este Procesare Declarații Clasa. Aici fiecare clasă avansează cu doua faze clasa in plus: Baze Procesate și Declarații Procesate. Mai întâi semantica încearcă sa rezolve clauzele extends/ implements din nume simple in nume complet calificate. Ordinea în care dependențele sunt rezolvate depinde atât de relația de moștenire cat și de cea de includere (nesting). Odată ce dependențele clasei sunt rezolvate, acestea sunt stocate într-o celulă temporara: · <unprocessedBases> - Inițializata cu lista de clase complet calificate pentru clasele menționate în clauzele extends/implements a clasei curente.

Odată ce <unprocessedBases> este salvata clasa intră în faza Baze Procesate. Clasa sta în această faza până când toate clasele menționate in clauzele extends/implements ajung in faza Declarații Procesate. Restricțiile din JLS asupra dependentelor dintre clase garantează ca între clase nu pot exista dependente ciclice, astfel clasa nu va rămâne blocata în starea de așteptare. Celula <unprocessedBases> este utilizata pentru a determina momentul în care clasa poate ieși din starea de așteptare. Odată ce o clasă ajunge în faza Declarații Procesata, ea este ștearsă din celula <unprocessedBases> a altor clase. Astfel, atunci când toate clauzele extends/implements a clasei ajung la faza Declarații Procesate, conținutul celulei <unprocessedBases> devine gol. Odată ce se ajunge in aceasta stare, clasa intră în faza Declarații Procesate si mai calculează trei celule: · <extends> - Clasa de baza complet calificata a clasei curente. · <implements> : Set[ClassType] - Lista de interfețe implementate direct, complet calificate. · <imports> Map[Id -> ClassType] - Un map al tuturor claselor accesibile prin nume simplu in interiorul clasei curente. Regulile de calcul ale acestui Map sunt complexe și includ următoarele surse:

○ Declarațiile import ale unității de compilare curente. ○ Clasele declarate în același package cu unitatea de compilare curentă. ○ Clasele accesibile în corpul clasei ce include clasa curentă, dacă clasa curentă

este internă altei clase. ○ Clase interne moștenite de la clasele de bază, adică de la clauzele

extends/implements.

61

○ Clase interne ale clasei curente.

Necesitatea de a acoperi toate aceste cazuri, duce la ordinea complexa in care trebuie rezolvate dependentele intre clase.

Atunci când o clasă intră faza declarații Procesate, celulele <rawExtends>, <rawImplements> și <unprocessedBases> nu mai sunt necesare și sunt șterse. După ce toate clasele ajung in aceasta faza computația trece in faza globala următoare.

În timpul etapei globale Procesare Membri Clasa fiecare clasă își procesează membrii și atinge în starea Membri Procesați. Pană în acel moment corpul clasei este stocat în <rawDeclarations>. Un membru a clasei poate fi una dintre: · câmp · metodă · constructor · inițializator static sau instanță

În această fază globală membrii claselor sunt distribuiți în următoarele celule: · <implTrans> : Set[ClassType] - închiderea tranzitivă a interfețelor implementate. În fazele rămase această mulțime este utilizata în relația de subtyping. · <methods> : Map[Signature -> ClassType] - Map-ul metodelor accesibile. Cheile sunt signaturi de metode, valorile sunt clasele în care sunt definite metodele. Include atât metode declarate în această clasă, cat și metode moștenite de la interfețele si clase de baza. · <methodDecs> : Map[Signature -> MethodClosure] - Map-ul metodelor definite. Valorile sunt de data aceasta implementări ale metodelor. Această celulă include doar metode definite în interiorul corpului de actuala clasă. · <fieldDecs> : AST - lista declarațiilor de câmpuri instanță, stocată ca și o listă de declarații de variabile locale fora inițializator. Utilizată în timpul instanțierii obiectelor. · <instanceEnv> : Map[Id -> FieldEntry] - aceleași câmpuri ca și în <fieldDecs> dar într-o alta forma. Utilizata în faza de elaborare. · <instanceInit> : AST - Lista de inițializatori instanță a clasei combinați într-un singur inițializator mare. Inițializatorii câmpurilor instanță sunt și ei concatenați în această celulă în ordinea lor textuală. Conținutul acestei celule este executat în cadrul instanțierii obiectelor. · <staticEnv> : Map[Id -> Location] - Map de la câmpuri statice declarate în această clasă la locația lor in <store>. Din moment ce câmpuri statice au o singură instanță per declarație de clasă, este posibil de a aloca o valoare în memorie pentru ele în această fază, atunci când câmpurile statice sunt detectate pentru prima oară. · <staticInit> : AST - Lista de inițializatori statici și inițializatori ai câmpurilor statice concatenați într-un singur bloc. Invocat în timpul inițializării statice a clasei. · <constantEnv> : Map[Id -> Value] - Un map de la constante la valorile lor. Constante în Java au o semantica ușor diferită față de câmpurile statice finale. În special, accesarea lor nu declanșează inițializarea statică a clasei ce le declară.

După ce toate celulele de mai sus sunt calculate clasa trece in faza Membri Procesați, iar celula <rawDeclarations> este ștearsa.

Ultima faza de preprocesare este Elaborarea. Aici sunt procesate toate blocurile de cod

62

- corpurile metodelor și constructorilor, inițializatorii statici și instanța. Cea mai mare parte a informației tradițional inferate de către compilator este calculata la aceasta fază. Mai exact în timpul elaborării sunt efectuate următoarele transformări: · Fiecare nume este rezolvat în variabila locală, câmp, metoda, clasa sau package. Dacă metodele pot fi distinse de alte categorii pur sintactic, rezolvarea în alte categorii necesită cunoașterea numelor existente în contextul curent. · Numele de clasă simple sunt rezolvate în nume complet calificate. De aici încolo toate numele de clase din cod sunt complet calificate. · Este dedus tipul la momentul compilării pentru fiecare expresie. Așadar, atunci când codul ajunge în faza de execuție el nu mai este în forma inițiala. Expresiile sunt adnotate cu tipul lor. · Pentru fiecare apel de metoda este dedusa signatura exacta. · Sunt procesate clasele locale si anonime. Cea mai timpurie etapa în care clasele locale pot fi descoperite este cea de elaborare. Totuși clasele locale au toate facilitățile altor clase, deci trebuie trecute prin toate etapele de preprocesare. Întreaga preprocesare pentru clase locale este efectuata în etapa globala de elaborare.

Cu toate ca aceasta faza este cea mai complexa dintre toate, ea introduce puține celule noi. Majoritatea țin de clase locale. In interiorul <class> este introdusa doar o celulă nouă: · <enclosingLocalEnv> : Map[Id -> Type] - Un map de la variabilele locale ale blocului curent la tipuri. Utilizat în procesarea claselor locale.

Dintre celulele globale sunt adăugate următoarele: · <elabEnv>: List[Map[Id -> Type]] - O stivă în care fiecare nivel este un map de variabile locale. Fiecare nivel din stiva reprezintă un bloc de cod, în ordinea imbricării blocurilor. In fiecare nivel map-ul este de la variabile locale accesibile în acel nivel la tipuri de variabile. · <localTypes>: List[Map[Id -> ClassType]] - O celulă similară ca structură cu celula anterioară. De data aceasta cheile map-ului sunt clase locale, nu variabile. · <nextLocalId>: Int - un număr utilizat pentru a genera nume complet calificate pentru clasele locale. În timpul fazei de elaborare nu este consumată nici o celula. Mai curând, blocurile de cod stocate în <methodDecs>, <instanceInit>, <staticInit> sunt procesate și stocate din nou în aceeași celula. După elaborare clasele rămân în aceeași stare -- Membri Procesați. Starea Membri Procesați este de fapt starea finală a celulei <class>.

Atunci când evaluarea ajunge la etapa finală, execuția, clasele mai au o celulă ce intră în joc: · <staticInitStatus> - un indicator al faptului dacă clasa curenta a fost sau nu inițializată static.

Printre celulele globale următoarele țin de etapa de execuție: · <store> : Map[Locatie:Int -> Valoare:ValoareTipizata] - memoria programului. Map de la locații de memorie către valori. Celula cea mai importantă introdusă în faza de execuție. · <nextLoc> : Int - Numărul de locații de memorie alocat. Utilizat pentru a genera adrese

63

unice de memorie la fiecare alocare. · <in> : Lista - intrarea standard, reprezintă o lista pre-parsată de valori Int sau String. · <out> : Lista – ieșirea standard. · <classLiteralsMap> : Map[Tip -> ValoareTipizata] - un map de la tipuri T la obiecte care reprezintă valoare expresiei T.class .

Celulele rămase țin de thread-uri: · <busy> : Set[Locatie:Int] - Mulțimea obiectelor ocupate. Adică obiecte monitor pentru care există un thread care deține monitorul. · <waitingThreads> : Map[ThreadId:Int -> Locatie:Int] - Map de la thread-uri la obiecte monitor pe care aceste thread-uri sunt "blocate în așteptare". Folosit de metodele Object.wait(), Object.notify(), Object.notifyAll(). · <terminated> : Set[ThreadId:Int] – Mulțimea thread-urilor terminate. Restul celulelor globale țin de depanare. 2.6.3 Cink (https://github.com/kframework/cink-semantics) Cink [LS13] este un nucleu al limbajului C++ definit în K pentru scopuri didactice şi de cercetare. Cink se deosebeşte de celelalte limbaje definite cu scop didactic (a se vedea mai jos) prin aceea că se doreşte predarea şi studierea conceptelor specifice limbajelor de programare reale. Fiecare trăsătură de limbaj definită în Cink pleacă de la descrierea sa din manualul de C++. Limbajul C++ este încă foarte popular, se dezvoltă continuu şi are câteva trăsături pe care nu le întâlnim la alte limbaje: punctele de secvenţiere (relaţia sequence before) care induc o relație de ordine parţială peste evaluarea subexpresiilor şi a efectelor secundare (side effects), clasificarea subexpresiilor în lvalues şi rvalues, apelul prin referinţă, pointeri şi relaţia acestora cu tablourile, etc. Din acest motiv constituie un limbaj foarte interesant de studiat şi a început să fie luat ca şi caz de studiu pentru alte platforme (Peter D. Mosses and Ferdinand Vesely. FunKons: Component-Based Semantics in K, trimisă la WRLA 2012). Cink este utilizat ca material didactic la universităţile din Iaşi (UAIC) şi Bucureşti (UB). 2.6.4 Alk (https://github.com/kframework/alk-semantics) Alk este un limbaj algoritmic proiectat pentru a fi utilizat la cursurile de predarea algoritmilor şi analiza acestora. O caracteristică principală a limbajului Alk o constituie simplitatea şi flexibilitatea în descrierea algoritmilor. Limbajul utilizează o implementare simplă de tipuri abstracte de date, astfel utilizatorul este eliberat de descrierea detaliilor de implementare acestora. Definiţia lui Alk permite executarea de specificaţii algoritmi descrise la un nivel de abstractizare ce permite focalizarea pe ideea algoritmică şi nu pe detaliile de implementare a acestora. În acelaşi timp Alk constituie un model de calcul ce permite definiţia riguroasă a funcţiilor de complexitate timp şi spaţiu. Definiţia lui Alk poate fi extinsă pentru a calcula automat aceste funcţii de complexitate pentru anumite categorii de algoritmi. Definiţia limbajului este în progres. 2.6.5 IMP (https://github.com/kframework/k/blob/master/samples/imp-abstract/no-env/imp.k ) IMP este un limbaj folosit în multe manuale și lucrări, de multe ori cu mici variații sintactice și de

64

multe ori fără a fi numit IMP. Acesta include construcțiile de bază ale paradigmei de programare imperativă: expresii aritmetice și booleene, atribuiri, instrucțiuni condiționale și iterații precum și compunerea secvențială. Descrierea sintaxei și semanticii limbajului IMP se află la: http://www.kframework.org/imgs/releases/k/tutorial/1_k/2_imp/lesson_5/imp.pdf 2.6.6 IMP++ (https://github.com/kframework/k/tree/master/samples/imp-abstract/with-env) IMP++ este extensia limbajului IMP pentru a suporta fire de execuție. În IMP++ este implementat un mecanism simplu de sincronizare a firelor de execuție: se adaugă id-uri unice pentru firele de execuție, se adaugă expresia spawn care returnează id-ul firului nou creat și instrucțiunile halt și join. 2.6.7 SIMPLE (https://github.com/kframework/k/tree/master/tutorial/2_languages/1_simple ) SIMPLE este un limbaj didactic și de cercetare, care surprinde esența paradigmei de programare imperativă, extins cu mai multe caracteristici de multe ori întâlnite în limbaje de programare imperative. Un program constă dintr-un set de declarații de variabile globale și definițiile funcțiilor. Ca și în C, definițiile de funcții nu pot fi imbricate și fiecare program trebuie să aibă o funcție numită main(), care este invocată atunci când programul este executat. Pentru a sublinia unele dintre punctele forte ale frameworkului K, SIMPLE include următoarele caracteristici, în plus față de stilul imperativ convențional următoarele trăsături: tablouri multidimensionale și referințe la tablouri, funcții și valori funcții, blocuri cu elemente locale, intrări/ieșiri, excepții, concurență prin crearea/distrugerea de fire de execuție cu sincronizare. 2.6.8 KOOL (https://github.com/kframework/k/tree/master/tutorial/2_languages/2_kool/1_untyped) KOOL este un limbaj care surprinde esența paradigmei de programare orientate obiect și este destinat pentru scopuri didactice și de cercetare. Un program în limbajul KOOL constă dintr-un set de declarații de clasă. Fiecare clasă poate prelungi cel mult o altă clasă (KOOL este un limbaj cu o singură moștenire). O clasă poate declara un set de domenii și un set de metode, toate fiind publice și numite membri ai clasei. Sintaxa limbajului KOOL extinde pe cea a limbajului SIMPLE prin adăugarea trăsăturilor orientate obiect. Descrierea sintaxei și semanticii limbajului KOOL se află la: http://www.kframework.org/imgs/releases/k/tutorial/2_languages/2_kool/1_untyped/kool-untyped.pdf. 2.6.9 FUN (https://github.com/kframework/k/tree/master/tutorial/2_languages/3_fun/1_untyped) FUN este un limbaj utilizat în scopuri didactice și de cercetare, care surprinde esența paradigmei de programare funcțională, extins cu mai multe caracteristici de multe ori întâlnite în limbaje de programare funcțională. Ca în multe limbaje funcționale, un program în FUN, inclusiv programul principal, este o expresie. Funcțiile pot fi declarate oriunde și sunt valori de primă clasă în limbaj. FUN este un limbaj care implementează apelul prin valoare dar a fost extins, în cadrul proiectelor date studenților, și cu alte stiluri de transmitere a parametrilor.

65

2.6.10 JVM (https://github.com/kframework/jvm-semantics) Definiţia lui Java Virtual Machine (JVM) este în progres. Au fost deja stabilită structura configuraţiei şi implementate funcţionalităţile de bază. Acum se lucrează la definiţia claselor şi obiectelor. O temă interesantă care va fi investigată după descrierea completă a definiţiei este stabilirii echivalenţei dintre semantica unui program Java (definită utilizând definiţia K a limbajului Java) cu semantica a versiunii compilate cu JVM (utilizând definiţia K a lui JVM). Iniţial această relaţie va fi verificată prin testare, apoi vom avea in vedere o demonstrare la nivel de definiţii. Definiţia lui JVM constituie subiecte de dizertaţie de master.

2.7. Demonstrator CIRC înglobat în K Framework CIRC [LGC09] este un demonstrator automat care implementează sistemul de deducție de coinducție circulară definit în [RL09]. Coinducția circulară este un sistem format din trei reguli de deducție care s-a dovedit eficient în demonstrarea de proprietăți coinductive, numite de multe ori și comportamentale.

CIRC a fost utilizat cel mai mult pentru a dovedi echivalența de definiții alternative pentru obiecte infinite, numită și echivalență comportamentală, cum ar streamurile, arborii infiniți, procese specificate algebric (ABP), dar și pentru obiecte finite cum ar fi expresiile regulate. O provocare in prezentul a fost aceea de a investiga în ce măsură coinducția circulară și tehnica de implementare utilizată în CIRC poate fi extinsă/adaptată/reproiectată pentru a putea demonstra proprietăți comportamentale ale programelor. Așa cum era de așteptat, prima proprietate care s-a avut în vedere a fost echivalența de programe, care poate fi privită ca un caz particular de echivalență comportamentală. Specificațiile de limbaje de programare în K sunt total diferite de specificațiile ecuaționale considerate în CIRC. În plus, noțiunea de derivativă utilizată în CIRC este dată direct sub forma unor operații peste ecuații, iar pentru programe aceasta trebuie definită în termenii relației de tranziție ce exprima execuțiile posibile ale programului. Definiția echivalenței de programe este dependentă de limbaj și cunoaște multe variante. Din aceste motive, utilizarea directă a CIRCului și a sistemului de coinducție circulară definit în [RL09] pentru programe s-a dovedit imposibilă de realizat și s-au pornit investigații pentru a adapta sistemul de coinducție circulară pentru specificațiile K și a de a găsi o definiție potrivită pentru noțiunea de derivativă. Punctul de plecare l-a constituit execuția simbolică care a permis ridicarea definiției relației de tranziție peste configurații concrete la o

66

relație de tranziție peste formule. Aceasta a permis să definim derivativa unei formule ce descrie configurația curentă ca fiind mulțimea de formule (interpretată ca disjuncție) ce pot fi obținute prin aplicarea regulilor din definiția limbajului. Noțiunea de echivalență de programe pe care am considerat-o este bazată pe cea de bisimilaritate și poate fi aplicată atât programelor care se termină cât și programelor cu execuții infinite (cum ar fi un sistem de operare, de exemplu). Sistemul de deducție obținut pentru noul context teoretic este cel publicat la IFM 2013 [LR13a]:

Mulțimea de formule Ω definește relația de observabilitate (când două configurații sunt observate ca fiind egale). Chiar dacă cele două sisteme sunt sintactic foarte asemănătoare, ceea ce e firesc deoarece ideea de bază este aceeași, semantic ele diferă prin modul de definire a mulțimii de derivative Δ și a relației de deducție de start ├. Demonstrarea corectitudinii sistemului deductiv se face într-un mod cu totul diferit iar în cazul echivalenței de programe s-a dovedit a fi mult mai dificilă. Execuția simbolică a fost extinsă la relație de rescriere cu unificare iar sistemul de deducție a fost rafinat în [LR13b] astfel încât să poată fi utilizat și pentru programe simbolice (când anumite părți din program sunt reprezentate prin variabile):

Definiția echivalenței de programe a fost reformulată cu ajutorului logicii temporale liniare iar corectitudinea sistemului deductiv a fost mult simplificată prin reducerea la dovedirea existenței unei execuții care satisface o formulă temporala liniară. Atât relația de observabilitate cât și relația de deducție de start depind de limbaj, face ca implementarea coinducției circulare în cadrul K să nu mai poată fi implementată la același nivel de generalitate. Au fost construite două prototipuri: unul pentru limbaj imperativ și altul pentru limbaj funcțional ce permite descrierea de programe cu execuții infinite (corecursive). Deoarece versiunea actuală a K-toolului se bazează pe Maude în sensul că specificația executabilă obținută este executată de sistemul Maude, realizarea celor două prototipuri a

67

necesitat implementarea sistemul de deducție direct în K prin extinderea definiției limbajului cu capabilitatea de a executa concurent perechi de programe, de a memora ipotezele circulare F, relația de subsumare dintre o conjectura curentă și mulțimea de ipoteze circulare. Ambele prototipuri pot fi executate ca definiții K utilizând interfața online a toolului K: http://fmse.info.uaic.ro/tools/K/?tree=examples/prog-equiv/README. Realizarea unui motor de rescriere bazat pe sistemul deductiv Reachability Logic va permite și o implementare generică a sistemului pentru echivalența de programe. Acestea sunt planificate pentru munca de cercetare din viitorul apropiat. Sistemul de deducție pentru echivalențe de programe este la nivel teoretic mai general decât cel din CIRC deoarece urmează un șablon de formulă temporală mai general. Ideea de raționament circular din CIRC a fost încorporată și în sistemul deductiv pentru Reachability Logic (inițial numită Matching Logic = Logica potrivirilor) [RS12a]. Regula de circularitate din acel sistem este în esență aceeași cu cel de la coinducția circulară numai că aplicată în contextul unei logici pentru corectitudinea parțială a programelor. Aceasta demonstrează că încorporarea raționamentului circular din CIRC în cadrul K se poate face într-un context mult mai larg decât cel a echivalenței de programe, ideea originală de la care s-a plecat la propunerea proiectului. Proprietatea de productivitate pentru specificațiile comportamentale (cele utilizate în CIRC) a fost studiată în [RL14] iar demonstratorul descris în [GLO14] are la bază o parte din tehnica utilizată la implementarea CIRCului. Toate aceste rezultate arată că raționamentul circular descris inițial în [R00] și apoi descris ca sistem de deducție în [RL09] are încă potențial neexplorat și aplicarea lui la studierea proprietăților de programe este foarte promițătoare. Argumentul cel mai puternic care susține această afirmație este dat de rezultatele fundamentale obținute și implementate lor la nivel de prototip în cadrul acestui proiect. Pentru a înțelege diferența dintre CIRC și implementarea coinducției circulare în K, considerăm următorul program corecursiv:

și presupunem că dorim să dovedim următoarea echivalență:

Reprezentarea acesteia în limbajul STREAM definit în K este dată ca o echivalență de configurații: <k> L.morse </k> <sspecs> not(xs) :~ 1 <| hd(xs) = 0 |> 0 : L.not(tl(xs)); zip(xs, ys) :~ hd(xs) : L.zip(ys, tl(xs)); morse :~ 0 : L.1 : L.zip(tl(L.morse), not(tl(L.morse)));

68

</sspecs> ~ <k> L.f(morse) </k> <sspecs> neg(x) := 1 <| x = 0 |> 0; not(xs) :~ 1 <| hd(xs) = 0 |> 0 : L.not(tl(xs)); zip(xs, ys) :~ hd(xs) : L.zip(ys, tl(xs)); f(xs) :~ hd(xs) : L.neg(hd(xs)) : L.f(tl(xs)); morse :~ 0 : L.1 : L.zip(tl(L.morse), not(tl(L.morse))); </sspecs> ; (https://github.com/kframework/k/tree/master/samples/prog-equiv/streams) Dovedirea acestei echivalențe cu implementarea K a coinducției circulare este similară celei pentru execuția de programe: $ kompile seq.k $ krun programs/morse.seq <T> <goals> .Bag </goals> <hypos> <hypo> <patt1> <hout1> 0 : [] </hout1> <hk1> 1 : (L . (f ( (((L . 1) : (L . (zip ( ((tl ( (L . morse) )), ((not ( ((tl ( (L . morse) )), .List{","}) )) , .List{","})) )))), .List{","}) ))) </hk1> </patt1> <patt2> <hout2> 0 : [] </hout2> <hk2> 1 : (L . (zip ( ((tl ( (L . morse) )), ((not ( ((tl ( (L . morse) )), .List{","}) )), .List{","})) ))) </hk2> </patt2> </hypo> <hypo> <patt1> <hout1> [] </hout1> <hk1> f(morse)

69

</hk1> </patt1> <patt2> <hout2> [] </hout2> <hk2> morse </hk2> </patt2> </hypo> </hypos> </T> Faptul că în configurația finală celula goals este vidă arată că demonstrația a reușit. Celula hypos include echivalența originală și o lemă (circularitate) descoperită și demonstrată. CIRC utilizează specificațiile ecuaționale pentru reprezentarea programelor corecursive: (theory BIT is sort Bit . ops 0 1 : -> Bit . var B : Bit . op not : Bit -> Bit . eq not(0) = 1 . eq not(1) = 0 . eq not(not(B)) = B . op _+_ : Bit Bit -> Bit [assoc comm] . eq B + 0 = B . eq B + B = 0 . eq B + not(B) = 1 . endtheory) (theory BITSTREAM is including BIT . sort Stream . vars S S' : Stream . --- destructors op hd : Stream -> Bit . op tl : Stream -> Stream . --- zip of streams op zip : Stream Stream -> Stream . eq hd(zip(S,S')) = hd(S) . eq tl(zip(S,S')) = zip(S',tl(S)) . --- complements a Bit stream op not : Stream -> Stream . eq hd(not(S)) = not(hd(S)) . eq tl(not(S)) = not(tl(S)) .

70

--- alternative function op f : Stream -> Stream . eq hd(f(S)) = hd(S) . eq hd(tl(f(S))) = not(hd(S)) . eq tl(tl(f(S))) = f(tl(S)) . --- Thue-Morse seqence M = 0:zip(inv(M),tail(M)) op morse : -> Stream . eq hd(morse) = 0 . eq hd(tl(morse)) = 1 . eq tl(tl(morse)) = zip(tl(morse), not(tl(morse))) . --- derivatives derivative hd(*:Stream) . derivative tl(*:Stream) . endtheory) Rezultatul întors de demonstratorul CIRC este: Goal added: f(morse) = morse rewrites: 16336 in 72ms cpu (73ms real) (226876 rewrites/second) Grlz [* f(tl(morse)) *] = [* zip(tl(morse),not(tl(morse))) *] to [* zip(V0:Stream,not(V0:Stream)) *] = [* f(V0:Stream) *] Proof succeeded. Number of derived goals: 8 Number of proving steps performed: 44 Maximum number of proving steps is set to: 256 Proved properties: zip(not(V0:Stream),tl(V0:Stream)) = tl(f(V0:Stream)) zip(V0:Stream,not(V0:Stream)) = f(V0:Stream) tl(f(morse)) = tl(morse) f(morse) = morse Observăm că CIRC a avut nevoie de o generalizare (linia care începe cu Grlz) și de trei leme suplimentare pentru a dovedi aceeași proprietate. Asta arată că implementarea motorului de coinducție circulară poate fi mai eficient în K.

71

2.8. Monografie

2.8.1 Programming Language Design and Semantics. Traian Florin Șerbănuță. Editura Universității Alexandru Ioan Cuza Iași, 2012 Această carte demonstrează că rescrierea oferă un cadru natural pentru definirea in mod formal a semanticii limbajelor de programare concurente folosite în industrie, precum și pentru testarea și analizarea programelor scrise în aceste limbaje, aducând următoarele contribuții-cheie în domeniul proiectării și analizei limbajelor de programare:

1. Coroborează dovezile existente și aduce noi dovezi pentru a demonstra că rescrierea în general, și logica rescrierii în particular, reprezintă un cadru potrivit pentru definirea semanticii limbajelor de programare și pentru executarea, explorarea, și analiza execuțiilor programelor scrise în aceste limbaje. Mai precis, logica rescrierii este reafirmată ca o platformă puternică și meta-logică pentru limbaje de programare, capabilă de a captura platformele de definirea a limbajelor existente cu o distanță minimă de reprezentare, și de a le oferi executabilitate și alte instrumente puternice de analiză.

2. Avansează platforma K, bazată pe rescriere, ca un candidat pentru o platformă ideală de definire a limbajelor, exemplificând puterea sa de abstracție și expresie în conjuncție cu capacitatea sa naturală de a captura concurența împreună cu modularitatea, flexibilitatea și simplitatea sa.

3. Arată că definițiile K pot fi transformate ușor în unelte de verificare a execuțiilor care pot fi folosite pentru a verifica proprietăți cum ar fi protecția accesului la memorie și buna sincronizare a firelor de execuție, sau pentru a testa și explora comportamente ale modelelor relaxate de memorie precum x86-TSO [OSS09]..

4. Înzestrează platforma K cu o semantică cu adevărat concurentă cu partajarea resurselor care permite capturarea în cadru platformei a granularității dorite pentru concurența firelor de execuție, în plus față de paralelismul deja oferit de regulile de deducție ale logicii rescrierii.

5. Descrie teoria și implementarea programului K-Maude, o implementare de referință a platformei K în logica rescrierii, care dă viață definițiilor K, și care a fost folosit pentru a da semantică unor limbaje de programare reale și pentru a deriva instrumente de analiză a programelor direct din definițiile limbajelor.

Structura cărții Capitolul 2 oferă o introducere sumară în logica rescrierii, necesară pentru înțelegerea celorlalte următoarelor capitole din carte și prezintă informații generale despre rescrierea de grafuri, necesare pentru înțelegerea materialului prezentat în capitolul 6. Capitolul 3 descrie într-un cadru uniform cele mai populare metodologii de definire a semanticii operaționale pentru limbaje de programare: semantica naturală [Kah87], semantica operațională structurată (SOS) [Plo04], modular SOS [Mos04], semantica bazată pe reducere cu contexte de evaluare [WF94] și mașina chimică abstractă (Cham) [BB92]. Se arată apoi că

72

fiecare dintre acestea poate fi reprezentată în logica rescrierii, folosind ca exemplu definiția unui limbaj de programare imperativ simplu. Mai mult, aceste metodologii sunt comparate între ele, analizând și prezentând punctele lor forte și slabe. Capitolul 4 oferă o privire de ansamblu asupra platformei K. Pornind de la o descriere intuitivă, bazată pe exemple, a platformei K, acest capitol arată cum limbajul K poate fi folosit pentru definirea atât a semanticilor statice pentru limbaje de programare cât și a celor dinamice și cum definițiile existente pot fi extinse în mod modular. Tehnica K este apoi detaliată explicând cum rescrierea poate fi folosită pentru a defini semantica limbajelor de programare folosind configurații de celule imbricate, computații și reguli (K) de rescriere. Capitolul se încheie prin prezentarea definiției limbajului AGENT, care începe ca un limbaj de expresii la care se adaugă iterativ trăsături funcționale, imperative, de control, de concurență cu fire de execuție și multi-agent și generare de cod. Scopul acestei definiții complexe este de a provoca formalismele existente de definire a limbajelor de programare și în același timp de a scoate în evidență puterea de expresie și modularitatea oferită de platforma K. Capitolul 5 arată cum definițiile K pot fi transformate ușor în instrumente de verificarea execuțiilor programelor scrise în limbajele respective. Acest capitol se deschide cu definiția limbajului KernelC, un sub-limbaj al limbajului de programare C, care conține funcții, alocare de memorie, aritmetica peste locații de memorie și directive de intrare/ieșire, și care poate fi folosit pentru executarea și testarea unor programe C reale. Apoi, se arată cum prin efectuare unor ajustări minore asupra acestei definiții se poate obține un instrument de analiză a execuțiilor pentru verificarea siguranței accesului la memorie. Apoi, limbajul KernelC este extins cu fire de execuție și directive de sincronizare, și două semantici concurente sunt propuse ca extensii a semanticii sale secvențiale. Prima semantică definește un model de memorie secvențial și poate fi ușor transformată într-un instrument de verificare a bunei sincronizări a execuțiilor și a absenței posibilității de blocare, sau într-un instrument de monitorizare pentru a colecta secvența evenimentelor de interes ce pot fi obținute în timpul execuției unui program. A doua semantică definește un model relaxat de memorie bazat pe modelul de memorie x86-TSO. Prin explorarea execuțiilor unei implementări a algoritmului lui Peterson de excludere mutuală pentru ambele definiții, se demonstrează că algoritmul garantează excluderea mutuală pentru modelul consistent secvențial, dar nu o poate garanta pentru modelul de memorie relaxat. Capitolul 6 definește formal o semantică cu adevărat concurentă pentru platforma K care permite definițiilor K să captureze concurența cu partajarea resurselor așa cum este ea prezentă în limbajele cu fire multiple de execuție curente. Folosind asemănarea dintre regulile {K} și regulile de rescriere pe grafuri, rescrierea concurentă K este definită printr-o translatare a problemei într-un nou formalism de rescriere a termenilor ca grafuri, numit rescrierea K pe grafuri. După impunerea unor restricții rezonabile, se arată că rescrierea K pe grafuri permite un grad mai mare de concurență decât formalismele existente de rescriere a termenilor ca grafuri, rămânând în același timp serializabilă și corectă față de rescrierea normală a termenilor. Rescrierea K este astfel definită ca proiecția pe termeni a rescrierii K pe grafuri și este demonstrată serializabilitatea ei, precum și corectitudinea și completitudinea față de rescrierea normală a termenilor. Capitolul se încheie arătând cum concurența care se poate obține prin

73

rescrierea K poate fi capturată la nivel teoretic în logica rescrierii, folosind capacitatea logicii rescrierii de a captura rescrierea pe grafuri. Capitolul 7 descrie prototipul K-Maude, o implementare în Maude a reprezentării directe a platformei K în logica rescrierii. Această reprezentare are la bază notația și tehnica K prezentate în capitolul 4, oferind o reprezentare textuală ASCII pentru ele, precum și un compilator în motorul de rescriere Maude. Capitolul se deschide cu prezentarea reprezentării ASCII a notației matematice K, folosită pentru a scrie definiții \K în K-Maude. Apoi, K-Maude este prezentat din punctul de vedere al utilizatorului, insistând pe caracteristicile sale și modul de a le utiliza. Apoi, cele două translatări disponibile în K-Maude sunt prezentate: una implementând reprezentarea directă a definițiilor K ca teorii executabile în logica rescrierii și cealaltă transformând definițiile K în LaTeX pentru a putea genera documente PDF din ele.. În finalul cărții, capitolul 8 prezintă și analizează cercetări conexe cu cele prezentate în carte iar capitolul 9 prezintă concluziile cărții și subliniază direcțiile posibile de continuare a cercetării.

2.8.2 Tutorialul K Tutorialul K se poate consulta online la http://www.kframework.org/index.php/K_Tutorial. Acesta conține o serie de filme din care se poate învăța modul de utilizare a framework-ului K pentru definirea limbajelor. Structura acestui tutorial este: 1 K Overview 2 Learning K

2.1 Part 1: Defining LAMBDA 2.2 Part 2: Defining IMP 2.3 Part 3: Defining LAMBDA++ 2.4 Part 4: Defining IMP++ 2.5 Part 5: Defining Type Systems 2.6 Part 6: Miscellaneous Other K Features

3 Learning Language Design and Semantics using K 3.1 Part 7: SIMPLE: Designing Imperative Programming Languages 3.2 Part 8: KOOL: Designing Object-Oriented Programming Languages 3.3 Part 9: FUN: Designing Functional Programming Languages 3.4 Part 10: LOGIK: Designing Logic Programming Languages

Fiecare din secțiuni conține un număr de lecții video. De pildă secțiunea 4 - definirea limbajului IMP++ are structura:

Lesson 1, IMP++: Extending/Changing an Existing Language Syntax Lesson 2, IMP++: Configuration Refinement; Freshness Lesson 3, IMP++: Tagging; Superheat/Supercool Kompilation Options Lesson 4, IMP++: Semantic Lists; Input/Output Streaming Lesson 5, IMP++: Deleting, Saving and Restoring Cell Contents Lesson 6, IMP++: Adding/Deleting Cells Dynamically; Configuration Abstraction, Part 2 Lesson 7, IMP++: Everything Changes: Syntax, Configuration, Semantics

74

Lesson 8, IMP++: Wrapping up Larger Languages 2.8.3 Teze de doctorat Într-o primă teză de doctorat elaborată în cadrul proiectului se utilizează semantica operaţională pentru analiza şi verificarea programelor. Sunt folosite sistemele pushdown pentru descrierea semanticii operaţionale cu framework-ul K. Sunt descrise sistemele pusdown în termenii frameworkului K argumentând că semantica gramaticilor independente de context este, după Goguen, cel mai important şi general exemplu de semantică pentru o algebra iniţială multisortată. Relaţia de tranziţie a unui sistem pushdown este definită în K prin reguli de calcul. Se arată, de asemenea, cum se poate specifica în formalismul K, prin reguli structurale, structura de latice completă. Se demonstrează validitatea unei reguli de calcul obţinută via configuraţii ordonate laticeal, cea ce conduce la introducerea noţiunii de regulă de calcul implicit (implicit computational rule). Se arată în continuare că stările abstracte se pot descrie în mod natural în K utilizând paternuri date prin operatori şi variabile. Este tratat şi cazul sistemelor pushdown infinite precum şi a celor nedeterministe. Notând prin kP abstracţia (descrisă în K) a sistemului pushdown P, se demonstrează că sistemul de tranziţie definit de kP simulează pe cel definit de P. În paragraful intitulat Collecting Semantics, Pushdown Systems, and K, este abordată problema analizei/verificării unei proprietăţi într-o specificaţie K a unui sistem pushdown. Colectarea de informaţii pe durata execuţiei (unui program, sistem, etc.) are aplicaţii diverse în: transformarea programelor, detectarea de malware, model checking. Se justifică alegerea sistemelor pushdown pentru collecting semantics pentru ca apoi, considerând o codificare K a unui sistem pushdown, să se dezvolte o tehnică pentru (re)utilizarea definiţiei K în a obţine metoda de analiză/verificare. Regulile pentru collecting semantics sunt obţinute prin identificarea şi gruparea regulilor din kP care mimează un model de memorie partajată. Proprietatea ce trebuie verificată nu apare explicit în regulile stabilite, ea este incorporată în celula collect. Este dovedit faptul că în această nouă K reprezentare a sistemului P, calculul este finit. Concluzia este că celula collect conţine la sfârşitul calculului o reprezentare a urmei finite maximale din kP. Se investighează în continuare relevanţa studierii sistemelor pushdown în contextul semanticii limbajelor de programare. Dacă S este K-specificarea pentru semantica unui limbaj de programare iar P este un program în acest limbaj, atunci prin S[P] se notează instanţierea semanticii pentru programul P. Se arată cum se construieşte sistemul pushdown asociat lui P şi se emite conjectura că acest sistem şi S[P] sunt bisimilare (echivalente comportamental). Abstractizarea predicatelor este o tehnică cunoscută pentru construirea de modele abstracte pentru programe: se defineşte un set de predicate peste variabilele programului. Capitolul al patrulea se ocupă de abstractizarea predicatelor în K. Mai întâi se arată cum poate fi definită în K abstractizarea predicatelor prin specificarea unui sistem pushdown. Se defineşte un calcul abstract în K după care se dovedeşte că un calcul abstract pentru un program în limbajul SIM se termină şi produce graful de control al fluxului asociat programului. Următoarea propoziţie stabileşte că specificarea ca şi sistem pushdown asociată unui program SIM produce un sistem pushdown finit. Paragraful intitulat Trace semantics with predicate abstraction, arată cum se obţin urmele calculeleor abstracte folosind predicate abstracte. După ce se defineşte configuraţia abstractă se dau regulile structurale pentru iniţializarea şi terminarea unei execuţii abstracte într-un program SIM pentru ca apoi să fie precizate regulile K pentru collecting

75

semantics SIM prin predicate abstracte. Aceste reguli sunt explicate amănunţit, se dezvoltă un exemplu și se demonstrează corectitudinea definiţiei K a collecting semantics a limbajului SIM prin predicate abstracte cu privire la descrierea K a semantici. Un capitol special este dedicat instanţierii collecting semantics pentru specificarea unui sistem pushdown pentru analiza aliasurilor. Se introduce SILK, un limbaj de programare care suportă crearea de obiecte, variabile globale, static scope şi proceduri recursive cu variabile locale. Se descrie sintaxa precum și semantica abstractă a limbajului SILK pentru analiza alias. Se introduce un nou limbaj, Shylock, care este focusat pe raţionamente relative la structurile din heap – obiecte cu câmpuri. Se prezintă configuraţia K pentru noul limbaj şi este pusă în evidenţă aceasta ca o abstracţie pentru shape analysis. Regulile care implementează semantica concretă şi pe cea abstractă a limbajului Shylock sunt puse în evidență și este demonstrată o teoremă de bisimilaritate a sistemelor de tranziţie generate de specificarea K în care celula abs conţine <0>id respectiv <1>id după care se dezvoltă un exemplu de calcul abstract pentru un program scris în acest limbaj. Se discută model checker-ul sistemului Maude, și se specifică un model checker direct în K în vederea utilizării lui pentru semantica abstractă a programelor Shylock. Pentru asta se descrie o specificare K parametrică care are drept parametri un invariant-stare şi o K-specificare a unui sistem pushdown. O a doua teză de doctorat prezintă un sistem generic, modular, pentru proiectarea sistemelor incorporate. O instanță a acestui sistem o constituie nucleul analizorului WCET. Mai întâi se consideră un sistem de calcul complex, specificat în K printr-o configurație generală care conține toate entitățile semantice necesare pentru a captura comportarea sistemului. Este prezentată descompunerea configurației generale în subconfigurații concrete cât și modularizarea acestora într-un mediu de execuție abstract. Modulele obținute comunică via o mulțime de mesaje ce sunt trimise printr-o celulă specială de calcul. Ca o instanță a acestui sistem modular este descris analizorul WCET ca un set de module ce corespund limbajului procesor, memoriei cache și memoriei principale. Aceste module, care comunică prin mesaje predefinite, sunt descrise amănunțit. Metodologia generală de estimare pentru WCET cuprinde specificarea sintaxei si semanticii în framework-ul K, specificarea K pentru microarhitectură, propagarea simbolurilor, utilizarea implicită sau explicită a explorării stărilor. Un capitol special al tezei este dedicat definiției formale, utilizînd K, a unui limbaj de asamblare din familia MIPS, limbaj denumit aici SSRISC. Se introduce sintaxa limbajului, care conține instrucțiuni aritmetice, instrucțiuni de ramificare condiționată sau nu, instrucțiuni de încărcare și de stocare precum și instrucțiuni speciale. Se prezintă apoi, de asemenea folosind K, semantica limbajului. Este pus în evidență elementul cheie pentru acest lucru – stabilirea configurației limbajului. Semantica executabilă pentru limbajul introdus este prezentată prin reguli pentru inițializarea calculului, pentru lookup și update pentru regiștri, pentru registrul contor al programului, precum și pentru instrucțiuni. Sunt de asemenea date regulile semantice pentru instrucțiunile nop și break și este stabilită configurația K pentru memoria principală pentru ca apoi să fie descrise regulile semantice pentru preluarea datelor din memoria principală. Sistemul memoriei extinse este prezentat pe larg cu o justificare a separării între componentele memoriei. Este prezentată o configurație extinsă a modulului memoriei principale, sintaxa limbajului SSRISC adnotat precum și regulile semantice pentru instrucțiunile extinse. Extensia propusă este folosită pentru a construi starea inițială a programului și pentru a

76

facilita testarea semanticii limbajului. De asemenea este reiterat faptul că limbajul va fi folosit pentru definirea abstracțiilor pentru analiza timpului în programele incorporate. Se continuă cu un capitol dedicat modelării în K a memoriei cache. Într-o primă secțiune este descrisă memoria cache punând în evidență atât caracteristicile de organizare a acesteia, ca buffer rapid între CPU și memoria principală, cât și a celor funcționale, precum și influența pa care o are cache-ul asupra timpului de execuție a sistemelor software încorporate. În vederea modelării în K a memoriei cache se propune o reprezentare parametrică a comportării acesteia atât ca organizare cât și ca funcționalitate. Elementul cheie pus în evidență este informația relativ la vechimea asociată fiecărei linii cache. Aceasta este reprezentată printr-o celulă specială numită age, prin funcțiile de actualizare a vechimii și prin regulile de rescriere prezentate. Paragraful următor descrie modulul Instruction Caches care are rolul de a comunica cu modulul ce descrie semantica limbajului și cu cel al memoriei principale. Sunt prezentate tipurile de comunicare între modulele sistemului după care sunt descrise configurațiile memoriei cache pentru instrucțiuni și regulile K pentru comportarea acestora. Modulul Data Caches este descris folosind aceleași principii ca pentru modulul Instruction Caches. Este descrisă configurația corespunzătoare, este pusă în evidență subconfigurația care este partajată cu configurația memoriei cache pentru instrucțiuni, care are niște celule specifice. Se dau apoi regulile K pentru comportarea memoriei cache pentru date. În continuare se folosește descrierea modulară a unui sistem incorporat pentru a defini abstracțiile necesare analizei WCET. Ca reprezentare abstractă a unui program este folosit graful fluxului de control(control flow graph - CFG). Este introdusă o nouă configurație abstractă, cea care reprezintă un CFG iar regulile de extracție a unui CFG sunt prezentate separat. Aceste reguli presupun o nouă implementare a modulului ce descrie semantica limbajului, în speță se modifică regulile pentru instrucțiunile de ramificare și cele de salt necondiționat. Graful obținut, cu adnotații pentru limitele circuitelor, este folosit într-o procedură de desfășurare (unfolding) pentru a obține toate execuțiile circuitelor. Este descrisă configurația unfolder și sunt date regulile pentru unfolding, mai întâi pentru inițializarea unui circuit apoi pentru intrarea și ieșirea din acesta. Următorul capitol al tezei, intitulat Data-flow Abstractions for WCET Analysis, prezintă mai întâi problema detectării unui caz particular de drum eronat și apoi o codificare în K a metodei de analiză a intervalelor. Este dat și un exemplu de detectare a unui drum eronat folosind execuția semantică . Ultimul capitol al tezei modelează în K metoda de analiză WCET cunoscută sub numele ILP + AI. Se pornește de la reprezentarea concretă a unui sistem incorporat, descrisă în capitolele anterioare. În modulul K denumit ILP Constraints este descris în detaliu algoritmul de generare a constrângerilor pornind de la structura programului. Regulile pentru extragerea constrângerilor sunt prezentate după ce este descrisă configurația corespunzătoare. Abstracțiile pentru comportarea memoriei cache pentru instrucțiuni sunt descrise pe larg și este exemplificată o execuție pentru o comportare particulară. Un paragraf întreg prezintă implementarea metodei în frameworkul K. S-au făcut experimente pe programe din Mälardalen benchmark și sunt prezentate și interpretate rezultatele experimentelor. Alte trei subiecte de teze de doctorat sunt în stadiu avansat de elaborare: Andrei Arusoaie - Platforma independentă de limbaj pentru execuţia simbolică: teorie şi aplicaţii

77

Denis Bogdănaş - Semantica formală a limbajului Java Radu Mereuţă - Parsarea modulară a definiţiilor de limbaje de programare Susținerile publice ale acestor teze sunt planificate pentru toamna anului 2014.

3. Descrierea modului de îndeplinire a indicatorilor de rezultat

3.1 Locuri de muncă nou create datorită proiectului total Au fost create în total trei poziții CD. Descrierea lor este dată în secțiunea următoare. În plus, Departamentul de Informatică FII are vacante peste 30 de poziții.

3.2 Locuri de muncă nou create în CD datorită proiectului Locurile create și ocupate cu oameni care au lucrat la proiect: - poziția 18 conferențiar, state de funcții 2012/2013 ale Departamentului de Informatică FII, câștigată de Traian Florin Șerbănuță, concurs Februarie 2013 - poziția 37 lector, state de funcții 2012/2013 ale Departamentului de Informatică FII, câștigată de Ștefan Ciobâcă, concurs Februarie 2013 - asistent de cercetare, Departamentul de Informatică DII, câștigată de Andrei Arusoaie, concurs Noiembrie 2013

3.3 Publicații științifice rezultate din proiect

3.3.1. Publicații în conferințe și reviste cu proces de recenzare [RL14] Grigore Roșu, Dorel Lucanu. Behavioral Rewrite Systems and Behavioral Productivity. Festschrift in Honor of Kokichi Futatsugi, LNCS, 2014 [GLO14] Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi. On Automation of OTS/CafeOBJ Method. Festschrift in Honor of Kokichi Futatsugi, LNCS, 2014 [EHB14] Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Roșu, On the Complexity of Stream Equality, Journal of Functional Programming, 2014, To appear. [MR13] Jose Meseguer and Grigore Roșu, The Rewriting Logic Semantics Project: A Progress Report, Information and Computation, Volume 231, pp 38-69. 2013 [ALR13] Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. Language-Independent Program Verification Using Symbolic Execution. RR-8369, 22, INRIA, 2013 [ALR13b] Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. A Generic Framework For Symbolic Execution. Software Language Engineering, Indianapolis, SUA, 2013 [LR13b] Dorel Lucanu, Vlad Rusu. Program Equivalence by Circular Reasoning. RR-8116, versiunea 4, INRIA, 2013, trimis spre publicare la FAoC [LR13a] Dorel Lucanu, Vlad Rusu. Program Equivalence by Circular Reasoning. IFM, Lecture

78

Notes in Computer Science, 362-377, 2013 [BCG13] Marcello Bonsangue, Georgiana Caltais, Eugen Goriac, Dorel Lucanu, Jan Rutten, Alexandra Silva. Automatic equivalence proofs for non-deterministic coalgebras. Science of Computer Programming, 78, 9, 1324 -- 1345, 2013 [RSC13] Grigore Roșu and Andrei Stefanescu and Stefan Ciobaca, Brandon Moore. One-Path Reachability Logic. LICS'13, IEEE. 2013 [SCM13] Andrei Stefanescu, Stefan Ciobaca, Brandon Moore, Traian Florin Șerbănuță, Grigore Roșu. Reachability Logic in K. Technical Report http://hdl.handle.net/2142/46296, Nov 2013 [A13] Andrei Arusoaie. Engineering Hoare-Logic based Program Verification in K. In SYNASC’13, IEEE, Sep 2013, Timisoara, Romania, to appear. [RS 13] Grigore Roșu and Traian Florin Șerbănuță, K Overview and SIMPLE Case Study, K'11, ENTCS. 2013. To appear [SCR13] Traian Florin Șerbănuță, Feng Chen and Grigore Roșu, Maximal Causal Models for Sequentially Consistent Systems, RV'12, LNCS 7687, pp 136-150. 2013 [AȘE+12] Andrei Arusoaie, Traian Florin Șerbănuță, Chucky Ellison, Grigore Roşu. Making Maude definitions more interactive. In WRLA, volume 7571 of LNCS, 2012, pp. 83–98. [AV12] Andrei Arusoaie, Daniel Ionuţ Vicol. Automating Abstract Syntax Tree construction for Context Free Grammars. In SYNASC’12, ISBN 978-1-4673-5026-6, IEEE, 2012, p. 152-159, Timisoara, Romania. [LAȘ+12] David Lazar, Andrei Arusoaie, Traian Florin Șerbǎnuțǎ, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Roşu. Executing Formal Semantics with the K Tool. In FM, volume 7436 of LNCS, 2012, pp 267–271 [LȘR12] Dorel Lucanu, Traian Florin Șerbănuță, Grigore Roșu. K Framework Distilled. In WRLA, volume 7571 of LNCS, 2012, pp. 31–53 [LR12] Vlad Rusu, Dorel Lucanu. A K-Based Formal Framework for Domain-Specific Modelling Languages. FoVeOOS, Lecture Notes in Computer Science, 7421, 214-231, 2012 [RS12a] Grigore Roșu, Andrei Stefanescu. Checking Reachability using Matching Logic. Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), 555-574, 2012 [RS12b] Grigore Roșu, Andrei Stefanescu. Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP'12, LNCS 7392, pp 351-363. 2012

79

[RS12c] Grigore Roșu, Andrei Ștefănescu. From Hoare Logic to Matching Logic Reachability. FM'12, LNCS 7436, pp 387-402. 2012 [ȘR12] Traian Florin Șerbănuță, Grigore Roșu. A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. In ICGT, volume 7562 of LNCS, 294-310, 2012 [ABB12] Irina Asavoae, Frank de Boer, Marcello Bonsangue, Dorel Lucanu, Jurriann Rot, Bounded Model Checking of Recursive Programs with Pointers in K, WADT 2012, LNCS, 2012 [ȘAL+11] Traian Florin Șerbănuță, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, Grigore Roșu. The K Primer (version 3.3). In K'11, ENTCS. to appear [LR11] Vlad Rusu, Dorel Lucanu.K Semantics for OCL - a Proposal for a Formal Definition for OCL. In K’11, ENCTS. to appear [MG11] Radu Mereuță, Gheorghe Grigoraș, Parsing K definitions, In K’11, ENCTS. to appear [AAL11] Mihail Asavoae, Irina Asavoae, Using the Executable Semantics for CFG Extraction and Unfolding, 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2011, Timisoara, Romania, September 26-29, 2011, 123-127, 2011 [AAL10] Irina Asavoae, Mihail Asavoae, Dorel Lucanu, Path Directed Symbolic Execution in the K Framework, 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010, Timisoara, Romania, 23-26 September 2010, 133-141, 2010 [AA10] Irina Asavoae, Mihail Asavoae, Collecting Semantics under Predicate Abstraction in the K Framework, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, Lecture Notes in Computer Science, 6381, 123-139, 2010

3.3.2. Prezentări invitate și tutoriale [ALR13a] Andrei Arusoaie Dorel Lucanu Vlad Rusu. Symbolic Execution in the K Framework: Support and Applications. PAS 2013 - Second International Seminar on Program Verification, Automated Debugging and Symbolic Computation Beijing, China, October 23-25, 2013 [S13] Traian Șerbănuță. Programming Language Semantics using K --- true concurrency through term-graph rewriting - EPTCS, 110, 2013 [SL12] Dorel Lucanu and Traian Șerbănuță. Programming Language Design and Analysis using the K Framework, Tutorial at SYNASC 2012

80

http://synasc12.info.uvt.ro/tutorials/tutorial-k-framework [L12a] Dorel Lucanu. K Definitions as Push-down Specifications. Action IC0701, 9th MC and WG Meeting, Darmstadt, Germany, 2012 [L11a] Dorel Lucanu. Contributions to the K framework. Action IC0701, 7th MC+WG Meeting, 2nd Action Training School, Limerick, Ireland, 2011 [L11b] Dorel Lucanu. An Introduction to K Framework by Examples. Centrum Wiskunde & Informatica (CWI), March, 2011 [LR11] Dorel Lucanu, Grigore Roșu Circular Behavioral Reasoning, Centrum Wiskunde & Informatica (CWI), November, 2011 [L11c] Dorel Lucanu. An example based introduction to K. Second Romanian-Japanese Algebraic Specification Workshop, 2011 [L11d] Dorel Lucanu CIRC prover: an overview. Second Romanian-Japanese Algebraic Specification Workshop, 2011

3.3.3 Monografie [Șer12] Traian Florin Șerbanuță. Programming Language Design and Analysis: a rewriting approach. Editura Universității „Alexandru Ioan Cuza“, Iași, 2012

3.3.4 Rapoarte de cercetare [CLR13] Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Language-Independent Proof System for Mutual Program Equivalence, TR13-03, Alexandru Ioan Cuza University, Faculty of Computer Science, 2013 [LS12] Dorel Lucanu, Traian Florin Șerbanuță. CinK - an exercise on how to think in K. TR 12-03, Version 2, Alexandru Ioan Cuza University, Faculty of Computer Science, 2012 [SAL12] Traian Florin Șerbănuță, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Roșu, The K Primer (version 2.5),Technical Report, January 2012, http://fsl.cs.illinois.edu/pubs/k-primer-2012-v25.pdf [RSC12] Grigore Roșu, Andrei Stefanescu, Stefan Ciobaca, Brandon Moore. Reachability Logic. Technical Report http://hdl.handle.net/2142/32952, July 2012 [RS11b] Grigore Roșu, Andrei Stefanescu. Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework. Technical Report http://hdl.handle.net/2142/28357, November 2011

81

3.3.5 Teze de doctorat  

[MAs12]  Mihail  Asavoae.    Semantics-­‐Based  WCET  Analysis.  Alexandru  Ioan  Cuza  University  of  Iași,  Romania,  2012,  https://fmse.info.uaic.ro/publications/152/  

     

[MIA12] Măriuca Irina Asavoae. K Semantics for Abstractions. Alexandru Ioan Cuza University of Iași, Romania, 2012, https://fmse.info.uaic.ro/publications/151/

3.3.6 Prezentări la atelierele de lucru din cadrul proiectului K Workshop 2010 (http://www.kframework.org/K10/): Grigore Roșu, The K Framework: Overview and Current Status Dorel Lucanu, Modular defintions in K Traian Florin Șerbănuță, K-Maude: Overview and Current Status Andrei Arusoaie, On Compiling K Definitions Mihail Asavoae, WCET Estimation in K Irina Mariuca Asavoae, CEGAR in K : Past, Present, Future Topics on the K Framework, Iași, 10-15 Ianuarie 2011: Grigore Roşu , The K Framework from the Beginnings to the Present Andrei Arusoaie, Pre-compilation Phase in the K-Maude Tool Irina Măriuca Asăvoae, Abstract Interpretation in the K Framework Mihail Asăvoae, Rewrite Based Worst Execution Time Dorel Lucanu, CIRC Presentation K Workshop 2011 (http://www.kframework.org/K11/ ) Grigore Roșu: Overview of K Grigore Roșu: Overview of Matching Logic Traian Șerbănuță: A concurrent semantics for the K framework Traian Șerbănuță: From Language Definitions to (Runtime) Analysis Tools Adrian Riesco, Irina Mariuca Asavoae and Mihail Asavoae: Debugging Programs using the Language Definition Traian Șerbănuță: The K-framework Tool Chain: towards version 2.0: lessons learned and new perspectives Radu Mereuta and Gheorghe Grigoras: Parsing in K-framework Andrei Arusoaie and Traian Șerbănuță: Contextual transformation in K Framework Grigore Roșu and Traian Șerbănuță: SIMPLE: Defining Imperative Languages in K Grigore Roșu and Traian Șerbănuță: FUN: Defining Functional Languages in K Grigore Roșu, Mark Hills and Traian Șerbănuță: KOOL: Defining Object-Oriented Languages in K Mihail Asavoae, Dorel Lucanu and Grigore Roșu: Towards Semantics-Based WCET Analysis

82

Vlad Rusu and Dorel Lucanu: DSMLK Vlad Rusu and Dorel Lucanu: K Semantics for OCL - a Proposal for a Formal Definition for OCL Elena Naum: Automated heap pattern generation Mihail Asavoae: Using the Executable Semantics for CFG Extraction and Unfolding Mihail Asavoae: Micro-architecture Modeling for Timing Analysis: A Case Study Irina Mariuca Asavoae: Using Abstractions in the K Framework Irina Mariuca Asavoae: Simulating Simulations in the K Framework Summer School on Language Frameworks (https://fmse.info.uaic.ro/events/SSLF12/): 1. Andrei Arusoaie: OCL constraints evaluation on symbolic models 2. Vlad Rusu, Dorel Lucanu: Program Equivalence by Circular Reasoning 3. Denis Bogdanas: K Semantics of Java 4. Stefan Ciobaca: From small-step semantics to big-step semantics, automatically. 5. Grigore Roșu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore: Reachability Logic 6. Mihail Asavoae: Semantics-Based WCET Analysis 7. Irina Mariuca Asavoae: K Semantics for Abstractions

4. Articole în care este referit K (listă parțială, sursa Google Scholar) Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012. Run your research: on the effectiveness of lightweight mechanization. SIGPLAN Not. 47, 1 (January 2012), 285-296. José Meseguer, Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming, Volume 81, Issues 7–8, October–November 2012, Pages 721-781 Mark Hills, Paul Klint, Jurgen J. Vinju. RLSRunner: Linking Rascal with K for Program Analysis. Software Language Engineering Lecture Notes in Computer Science Volume 6940, 2012, pp 344-353 Maribel Fernández, Hélène Kirchner, Olivier Namet. A Strategy Language for Graph Rewriting. Lecture Notes in Computer Science Volume 7225, 2012, pp 173-188 Peter Dinges, Gul Agha. Scoped Synchronization Constraints for Large Scale Actor Systems. Lecture Notes in Computer Science Volume 7274, 2012, pp 89-103 Robert J. Simmons. Substructural Logical Specifications. PhD Thesis. CMU-CS-12-142 November 14, 2012 Robert J. Simmons, Frank Pfenning. Logical approximation for program analysis. June 2011, Volume 24, Issue 1-2, pp 41-80 Jeroen van den Bos, Mark Hills, Paul Klint, Tijs van der Storm, Jurgen J. Vinju . Rascal: From Algebraic

83

Specification to Meta-Programming. Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering (AMMSE 2011), Zurich, Switzerland, 30th June 2011, Electronic Proceedings in Theoretical Computer Science 56, pp. 15–32. M Hills. Streamlining Policy Creation in Policy Frameworks. WADT 2012 Preliminary Proceedings, 2012 Milos Gligoric, Darko Marinov, and Sam Kamin. 2011. CoDeSe: fast deserialization via code generation. In Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA '11). ACM, New York, NY, USA, 298-308. Camilo Rocha, Héctor Cadavid, César Muñoz, Radu Siminiceanu. A Formal Interactive Verification Environment for the Plan Execution Interchange Language. Lecture Notes in Computer Science Volume 7321, 2012, pp 343-357 Stephen T. Heumann, Vikram S. Adve, and Shengjie Wang. 2013. The tasks with effects model for safe concurrency. SIGPLAN Not. 48, 8 (February 2013), 239-250.

A Rizzi, Incremental reachability checking of KernelC programs using matching logic, PhD Thesis, Politecnico di Milano, 2013, https://www.politesi.polimi.it/bitstream/10589/85206/1/Incremental%20reachability%20checking%20of%20KernelC%20programs%20using%20matching%20logic.pdf

5. Referințe bibliografice (articole citate in raport dar care nu sunt produse in cadrul raportului sau au alți autori decât membri ai proiectului) [BB92] Gérard Berry and Gérard Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217-248, 1992. [DN04] Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. RS RS-04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004. [Esp95] David Espinosa. Semantic Lego. PhD thesis, Columbia University,1995. [FF86] Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. In 3rd Working Conference on the Formal Description of Programming Concepts, pages 193–219, Ebberup, Denmark, August 1986. [FWH01] Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages. MIT Press, Cambridge, MA, 2nd edition, 2001.

84

[ISO11] ISO/IEC JTC 1, SC 22, WG 14. ISO/IEC 9899:2011: Programming languages—C. Committee Draft N1570, International Organization for Standardization, August 2011. [Kah87] Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg,Guy Vidal-Naquet, and Martin Wirsing, editors, STACS 87, volume 247 of LNCS, pages 22–39. Springer, 1987. [Mes92] José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992. [Mog91] Eugenio Moggi. A modular approach to denotational semantics. In David H. Pitt, Pierre-Louis Curien, Samson Abramsky, Andrew M. Pitts, Axel Poigné, and David E. Rydeheard, editors, Category Theory and Computer Science, volume 530 of LNCS, pages 138–139. Springer, 1991. [Moo65] Gordon E. Moore. Cramming more components onto integrated circuits. Electronics, 38(8), April 1965. [Mos04] Peter D. Mosses. Modular structural operational semantics. Journal of Logic and Algebraic Programming, 60-61:195–228, 2004. [MPA05] Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In POPL'05. ACM Press. [MR04] José Meseguer and Grigore Roșu. Rewriting logic semantics: From language specifications to formal analysis tools. In IJCAR’04, volume 3097 of LNCS, pages 1–44. Springer, 2004. [MR06] José Meseguer and Grigore Roșu. The rewriting logic semantics project. In SOS’05, volume 156(1) of ENTCS, pages 27–56. Elsevier, 2006. [MR07] José Meseguer and Grigore Roșu. The rewriting logic semantics project. Theoretical Computer Science, 373(3):213–237, 2007. [OSS09] Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs, volume 5674 of LNCS, pages 391–407. Springer, 2009. [Plo04] Gordon D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17–139, 2004. Original version: University of Aarhus Technical Report DAIMI FN-19, 1981. [Ros03] Grigore Roșu. CS322, Fall 2003 - Programming Language Design: Lecture Notes. Technical Report UIUCDCS-R-2003-2897, University of Illinos at Urbana Champaign, December 2003. Lecture notes of a course taught at UIUC.

85

[RL09] Grigore Roșu, Dorel Lucanu. Circular coinduction – a proof theoretical foundation. In CALCO 2009, volume 5728 of LNCS, pages 127–144. Springer, 2009. [RS09] Grigore Roșu, Wolfram Schulte. Matching Logic - Extended Report. http://hdl.handle.net/2142/10790 Technical Report UIUCDCS-R-2009-3026, University of Illinos at Urbana Champaign, January 2009 [RES09] Grigore Roșu, Wolfram Schulte. From Rewriting Logic Executable Semantics to Matching Logic Program Verification. http://hdl.handle.net/2142/13159 Technical Report , University of Illinos at Urbana Champaign, July 2009 [RS11a] Grigore Roșu, Andrei Stefanescu. Matching Logic: A New Program Verification Approach (NIER Track) ICSE'11, ACM, pp. 868-871. 2011 [LGC09] Dorel Lucanu, Eugen Goriac, Georgiana Caltais, Grigore Roșu. CIRC : A Behavioral Verification Tool based on Circular Coinduction. CALCO 2009, LNCS, 5728, 433--442, 2009 [R00] G. Roșu. Hidden Logic. PhD thesis, University of California at San Diego, 2000. [Ros06] Grigore Roșu, K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation, Technical report UIUCDCS-R-2006-2802, December 2006. [�ŠA08] Jaroslav Ševčík and David Aspinall. On validity of program transformations in the Java memory model. In ECOOP, volume 5142 of LNCS, pages 27–51. Springer, 2008. [SSN+09] Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In POPL, pages 379–391. ACM, 2009. [WF94] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994. [GJS00] James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. Java Language Specification, Second Edition: The Java Series. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2nd edition, 2000. [HHK89] J. Heering, P. R. H. Hendriks, P. Klint, and J. Rekers, “The syntax definition formalism SDF—reference manual—,” SIGPLAN Not., vol. 24, no. 11, pp. 43–75, Nov. 1989. [JJ03] Jones, Joel: Abstract Syntax Tree Implementation Idioms. In: Proceedings of the 10th Conference on Pattern Languages of Programs (PLoP2003), 2003

86

[B03] Beck, K. Test-Driven Development by Example, Addison Wesley - Vaseem, 2003 Jump up ^ Lee Copeland (December 2001). "Extreme Programming". Computerworld. Retrieved January 11, 2011. [ACR98] Isabelle Attali , Denis Caromel , Marjorie Russo: A Formal Executable Semantics for Java Proceedings of Formal Underpinnings of Java - An OOPSLA'98 Workshop, Vancouver, October 1998. [FCM04] Azadeh Farzan, Feng Chen, Jose Meseguer, and Grigore Roșu. Formal analysis of java programs in javafan. In Proceedings of Computer-aided Verification (CAV'04), volume 3114 of LNCS, pages 501 - 505, 2004. [SBS01] Robert F. Stark, E. Borger, and Joachim Schmid. Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2001.