When you are writing intended functions involving complex objects, it is often necessary to use I/F lines that discuss in prose how those objects' states change. Here are some examples:
symbolTable := symbolTable with newSym added tapeDrive := tapeDrive rewound scrollBar := scrollBar positioned one page further down
Note that it is not necessary to be mathematical about every state change. You can use prose definitions so long as the meaning is clear.
For standard I/O streams, I use the notation <stdin>, <stdout>, and <stderr>. For example, here's the Python I/F code to write a string s to the standard output stream:
# [ <stdout> +:= s ] sys.stdout.write ( s )