Forfining (computing) - Refinement (computing)

Datatransformation
Begreber
Transformationssprog
Teknikker og transformationer
Ansøgninger
Relaterede

Forfining er et generisk udtryk inden for datalogi, der omfatter forskellige tilgange til produktion af korrekte computerprogrammer og forenkling af eksisterende programmer for at muliggøre deres formelle verifikation.

Programforfining

I formelle metoder er programforfining den verificerbare transformation af en abstrakt (højt niveau) formel specifikation til et konkret (lavt niveau) eksekverbart program . Trinvis forbedring tillader, at denne proces udføres trinvis. Logisk set involverer forfining normalt implikationer , men der kan være yderligere komplikationer.

Den progressive just-in-time forberedelse af produktets efterslæb (kravliste) i agile softwareudviklingsmetoder , såsom Scrum , er også almindeligt beskrevet som raffinement.

Forfining af data

Dataforfining bruges til at konvertere en abstrakt datamodel (f.eks. Med hensyn til sæt ) til implementerbare datastrukturer (såsom arrays ). Operationsforfining konverterer en specifikation af en operation på et system til et implementerbart program (f.eks. En procedure ). Den postcondition kan styrkes og / eller den forudsætning svækket i denne proces. Dette reducerer enhver ubestemmelse i specifikationen, typisk til en fuldstændig deterministisk implementering.

For eksempel kunne x ∈ {1,2,3} (hvor x er værdien af variablen x efter en operation) raffineres til x ∈ {1,2}, derefter x ∈ {1} og implementeres som x  : = 1. Implementeringer af x  : = 2 og x  : = 3 ville være lige så acceptabelt i dette tilfælde ved at bruge en anden rute til forfining. Vi skal dog være forsigtige med ikke at forfine til x ∈ {} (svarende til falsk ), da dette ikke kan implementeres; det er umuligt at vælge et medlem fra det tomme sæt .

Udtrykket reifikation bruges også undertiden (opfundet af Cliff Jones ). Afskærmning er en alternativ teknik, når formel forfining ikke er mulig. Det modsatte af raffinement er abstraktion .

Forbedringsregning

Refinement calculus er et formelt system (inspireret af Hoare-logik ), der fremmer programforfining. Den Fermat Transformation System er en industriel styrke implementeringen af raffinement. Den B-metode er også en formel metode , der strækker sig raffinement calculus med en komponent sprog: det har været brugt i industrielle udvikling.

Forfiningstyper

Hovedartikel: Forfiningstype

I typeteori er en forfiningstype en type udstyret med et predikat, som antages at holde for ethvert element af den raffinerede type. Forfining typer kan udtrykke forudsætninger , når de anvendes som funktionsargumenter eller postconditions når de anvendes som tilbagevenden typer : for eksempel, typen af en funktion, der accepterer naturlige tal og returnerer naturlige tal større end 5, kan skrives som . Forfiningstyper er således relateret til adfærdsmæssig undertypning .

Se også

Referencer