Tartalom
Induljunk ki egy olyan adatfile-ból amelyben azonos típusú elemek
találhatóak. Ezt a file-t törzsfile-nak fogjuk nevezni. Legyen az elemek típusa
,
ekkor
Legyen adott továbbá egy olyan file, amely transzformációk sorozatát
tartalmazza. Ezt a file-t fogjuk módosítófile-nak nevezni. Legyen
,
ekkor
A feladat az, hogy időszerűsítsük a törzsfile-t a módosítófile-ban leírt transzformációkkal. Jelölje
az időszerűsítés
transzformációt. Ekkor 
és
Ahhoz, hogy a feladatra megoldást adjunk ez a leírás még mindig túl általános, ezért további kikötéseket teszünk a file-okra.
Az időszerűsítés kulcsos
Legyen
és 
, ahol 
egy tetszőleges rendezett halmaz, a rekordok kulcsrésze;
a törzsrekord
adatrésze; 
pedig az elvégzendő transzformációt definiáló típus. Feltesszük
továbbá, hogy mind a tözsfile, mind a módosítófile a kulcsmező
(
) szerint
rendezett, azaz a 
és 
típusok invariáns tulajdonságára:
A törzsfile a kulcsmező szerint egyértelmű
A transzformáció csak az alábbi három féle lehet
Ahol a jelölés nem rontja el a szelektorfüggvények egyértelműségét, ott az egymás után következő szelektorfüggvény-sorozatból a közbülső elemek – a jelölést egyszerűsítendő – kihagyhatók, ezért pl. ha
, akkor
helyett
csak 
-t írunk.
Hátra van még annak leírása, hogy hogyan hatnak a fenti transzformációk a törzsfile-ra. Kényelmi okokból a transzformációk eredményét halmazként adjuk meg (ez elegendő, mert a törzsfile kulcs szerint egyértelmű). Ehhez bevezetünk néhány jelölést: legyen
, ahol
rendezett halmaz,
pedig tetszőleges
típus, valamint 
. Ekkor
ahol
A javítás művelet csere
Ebben az esetben a
típust
úgy szoktuk felírni, hogy a 
mező helyére 
-t írunk és a 
függvényalkalkalmazást a módosítórekord adatrészére
(
) cseréljük.
A feladat specifikációja tehát:
|
|
|
|
Ha a fenti specifikációban 
, akkor közönséges, ha 
akkor egyszerű időszerűsítésről beszélünk.