@prefix prodottidellaricerca: . @prefix istituto: . @prefix prodotto: . istituto:CDS044 prodottidellaricerca:prodotto prodotto:ID221890 . @prefix pubblicazioni: . @prefix unitaDiPersonaleEsterno: . unitaDiPersonaleEsterno:ID18934 pubblicazioni:autoreCNRDi prodotto:ID221890 . @prefix modulo: . modulo:ID2828 prodottidellaricerca:prodotto prodotto:ID221890 . @prefix rdf: . @prefix retescientifica: . prodotto:ID221890 rdf:type retescientifica:ProdottoDellaRicerca , prodotto:TIPO1101 . @prefix rdfs: . prodotto:ID221890 rdfs:label "A Framework for Automated and Certified Refinement Steps (Articolo in rivista)"@en . @prefix xsd: . prodotto:ID221890 pubblicazioni:anno "2012-01-01T00:00:00+01:00"^^xsd:gYear ; pubblicazioni:doi "10.1007/s11334-012-0183-6"^^xsd:string . @prefix skos: . prodotto:ID221890 skos:altLabel "
Griesmayer Andreas, Zhiming Liu, Morisset Charles, Shuling Wang (2012)
A Framework for Automated and Certified Refinement Steps
in Innovations in systems and software engineering (Internet); Springer-Verlag London Limited, London (Regno Unito)
"^^rdf:HTML ; pubblicazioni:autori "Griesmayer Andreas, Zhiming Liu, Morisset Charles, Shuling Wang"^^xsd:string ; pubblicazioni:paginaInizio "2"^^xsd:string ; pubblicazioni:paginaFine "12"^^xsd:string ; pubblicazioni:altreInformazioni "ID_PUMA: cnr.iit/2012-A0-002"^^xsd:string ; pubblicazioni:numeroVolume "1"^^xsd:string . @prefix ns11: . prodotto:ID221890 pubblicazioni:rivista ns11:ID97806 ; pubblicazioni:pagineTotali "10"^^xsd:string ; skos:note "Scopu"^^xsd:string ; pubblicazioni:affiliazioni "Imperial College, London, UK; International Institute for Software Technology - United Nations University; CNR-IIT, Pisa, Italy; Institute of Software, Chinese Academy of Sciences"^^xsd:string ; pubblicazioni:titolo "A Framework for Automated and Certified Refinement Steps"^^xsd:string ; prodottidellaricerca:abstract "The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma."@en . @prefix ns12: . prodotto:ID221890 pubblicazioni:editore ns12:ID12037 ; prodottidellaricerca:prodottoDi istituto:CDS044 , modulo:ID2828 ; pubblicazioni:autoreCNR unitaDiPersonaleEsterno:ID18934 . @prefix parolechiave: . prodotto:ID221890 parolechiave:insiemeDiParoleChiave . ns11:ID97806 pubblicazioni:rivistaDi prodotto:ID221890 . ns12:ID12037 pubblicazioni:editoreDi prodotto:ID221890 . parolechiave:insiemeDiParoleChiaveDi prodotto:ID221890 .