data specification using inode icache-entry := mkientry(. .dirty : bool;. .inode : inode) ; variables ie : icache-entry; end data specification