A megoldás definíciója kimondja majd, hogy a feladatban megfogalmazott feltételeknek csak azokra a végrehajtási utakra kell teljesülni, amelyekre teljesül a feltétlenül pártatlan ütemezés axiómája.
Egy végrehajtási útról azt mondjuk, hogy teljesül rá a feltétlenül pártatlan ütemezés axiómája, ha az út mentén a feltételes értékadások halmazából minden utasítás végtelen sokszor kerül kiválasztásra, azaz a címkefüggvény az út mentén a
indexhalmaz minden elemét végtelen sokszor rendeli az élekhez Megkövetelhetünk azonban kevesebbet is, pl.: hogy a feladatban megfogalmazott feltételeknek csak azokra a végrehajtási utakra kell teljesülni, amelyekre teljesül az utófeltételekre vonatkozóan pártatlan ütemezés axiómája..
Ha a konkrét, adott architektúrára leképezett programra teljesül, hogy feltétlenül pártatlan ütemezés mellett kerül végrehajtásra, akkor a többi utat valóban nem kell figyelembe venni a megoldás helyessége szempontjából. Ebben az esetben a program működése nemdeterminisztikus módon kiválasztott transzformációk iterációjával írható le, ahol a nemdeterminisztikusság véges de nem korlátos hasonló értelemben, ahogy relációk nem korlátos lezártjáról beszéltünk [[???Fót 83, ???Hor 90]]. Több utasítás közül ugyanaz az utasítás véges, de nem korlátos sokszor nem kerül kiválasztásra közvetlenül egymás után.
Utasítások pártatlan kiválasztására sokféle feltételt lehet megfogalmazni [[???Fra 86, ???And 91]], ezek közül az egyik leggyengébb a pártatlan ütemezés axiómája. Így feltétlenül pártatlan ütemezés mellett jól működő programok az általában szigorúbb ütemezési feltételek esetén is megoldják a feladatot.
Az ún. őrfeltételek [[???Dij 75, ???Hoa 78, ???And 91]] hasonlítanak a feltételes értékadásokban
szereplő
feltételekhez. A feltételes értékadások hatásrelációi azonban akkor is
definiáltak, ha az adott állapotra a feltétel nem teljesül. Ezért a
generált fában mindig megjelenik az értékadás hatásrelációjának
megfelelő él. A hamis őrfeltételű műveletek azonban nem generálnak
éleket.
Feltétlenül pártatlannak nevezünk egy ütemezést, ha minden őrfeltételhez nem kötött és végrehajtásra váró elemi művelet előbb utóbb végrehajtásra kerül (. def.).
Gyengén pártatlan egy ütemezés, ha feltétlenül pártatlan és minden olyan művelet, amelynek őrfeltétele igazzá válik és igaz is marad, előbb-utóbb végrehajtásra kerül.
Szigorúan pártatlan egy ütemezés, ha feltétlenül pártatlan és minden olyan elemi művelet, amely végrehajtásra vár és őrfeltétele végtelen sokszor igaz, előbb-utóbb végrehajtásra kerül.
21.24. Definíció (Utófeltételekre pártatlan ütemezés).
Nem teljesül egy végrehajtási útra az utófeltételekre vonatkozóan pártatlangyengén pártatlan ütemezés axiómája, ha - egy adott pontjától kezdődően minden pontjában kiválasztható olyan utasítás, amely az adott pontnak megfelelő állapotból egy adott logikai függvény igazsághalmazába visz és - sohasem kerül ilyen utasítás kiválasztásra.
A feltételes értékadások halmazaként definiált absztrakt program nem tartalmaz őrfeltételeket. A továbbiakban feltételezzük, hogy az implementált program végrehajtása feltétlenül pártatlan.
21.7. Megjegyzés.
Belátható, hogy feltétlenül pártatlan ütemezéssel nem pártatlan ütemezés is modellezhető [[???Cha Mis 89]].