A Formal Specification of Parlog