data specification using page pcache-entry := mkpentry(. .dirty : bool;. .page : buffer) ; variables pe : pcache-entry; end data specification