specification sorts ref; constants null : ref; variables r : ref; r0 : ref; r1 : ref; end specification