Absztrak read

sa, da, a : read ; \  sa = norm  / ; da =′ ′ ∧ sa = norm ; \overline{sa, da, a : read} ; \  sa = norm  / ; da ≠′ R′ ∧ sa = norm ∧ da ≠′ ′ ; \overline{sa, da, a : read} ; sx := norm ; \  sa = norm  / ; dx := da =′ R′ ; \  da ≠′ ′  / ; sa, da, a : read ; da ≠′ ′ ∧ sa = norm ; \overline{sa, da, a : read} ; SKIP ; dx :=↓ ; {sx := \atop abnorm} ; {sx := \atop abnorm}

i := m ; ¬β(i) ; \overline{i := i + 1}

tétel alapján.

Általában biztonságosabb, ha az absztrakt read nem olvasással indul. Olvasással fejeződik be, és ezért egy item feldolgozása elveszhet a következő absztrakt read műveletnél. A probléma elkerülhető, ha az absztrakt file open műveletében mindjárt egy item beolvasására is sor kerül. Ennek alapján az absztrakt file műveletek a következők:

Absztrak open

sa, da, a : read

Absztrak read

\frac{\  sa = norm  /}{da =′ ′ ∧ sa = norm ; \overline{sa, da, a : read} ; \  sa = norm  / ; da ≠′ R′ ∧ sa = norm ∧ da ≠′ ′ ; \overline{sa, da, a : read} ; sx := norm ; \  sa = norm  / ; dx := da =′ R′ ; \  da ≠′ ′  / ; sa, da, a : read ; da ≠′ ′ ∧ sa = norm ; \overline{sa, da, a : read} ; SKIP ; dx :=↓ ; {sx := \atop abnorm} ; {sx := \atop abnorm}}