Damnjanovic, Ljiljana B.2014-10-212014-10-2119911467-8659https://doi.org/10.1111/1467-8659.1010011In this paper the formal specification of a part of level la of GKS is given in the algebraic specification language OBJ. It shows that it is possible to produce a formal specification of a substantial part of GKS which is of manageable size and complexity specifying the appropriate level of abstraction of the system and using a suitable formal technique.10.1111/1467-8659.101001111-25