Det finns en stor samling operativa programvarusystem som är mycket viktiga för användarna, men som ändå blir allt svårare att underhålla, förbättra och hålla sig à jour med snabbt föränderliga krav. För många av dessa så kallade äldre system är alternativet att kasta bort systemet från en omskrivning från grunden inte ekonomiskt lönsamt. Det finns därför ett trängande behov av metoder som gör det möjligt för dessa system att utvecklas på ett kontrollerat sätt. Det tillvägagångssätt som beskrivs i detta dokument använder formella beprövade programomvandlingar, som bevarar eller förfinar semantiken i ett program samtidigt som dess form förändras. Dessa omvandlingar tillämpas för att omstrukturera och förenkla de äldre systemen och för att ta fram representationer på högre nivå. Genom att använda en lämplig sekvens av omvandlingar garanteras den extraherade representationen vara likvärdig med koden. Metoden bygger på ett formellt brett spektrumspråk, kallat WSL, med tillhörande formell metod. Under de senaste tio åren har vi utvecklat en stor katalog med beprövade transformationer, tillsammans med mekaniskt kontrollerbara tillämpbarhetsvillkor. Dessa har tillämpats på många mjukvaruutveckling, omvänd konstruktion och underhållsproblem. I detta dokument fokuserar vi på resultaten av att använda detta tillvägagångssätt i omvänd teknik av medelstor skala, industriell programvara, främst skriven på språk som monter och JOVIAL. Resultat från både referensalgoritmer och kraftigt modifierad, geriatrisk programvara sammanfattas. Vi drar slutsatsen att formella metoder har en viktig praktisk roll i mjukvaruutvecklingen.
En annan formalism för programomvandling är metoden baserad på WSL (Wide Spectrum Language) REF.
Formal Methods to Aid the Evolution of Software
{'venue': None, 'journal': None, 'mag_field_of_study': ['Computer Science']}