Ina Jo is a formal specification language. It is a non procedural assertion language that is an extension of first order predicate calculus. (NXR)
InaJo