generic specification
parameter
elem
using buffer
target
functions pack : elem → buffer;
unpack : buffer → elem;
axioms unpack : ⊦ unpack(pack(a)) = a;
used for: s, ls;
end generic specification