This Master s thesis discusses the development of OCL specifications for Java Card API, and is part of the KeY project. OCL is a specification language, i.e. it is used to express formally the requirements on a system. The KeY tool is a CASE tool, in which formal methods (formal specification and formal verification) are integrated with contemporary software development techniques. The main purpose of the OCL specifications is to simplify the verification of Java Card programs within the KeY tool. Verification means that one through mathematical and logical methods proves that the implementation fulfils the requirements in the specification. Already existing specifications written in JML, a specification language specially suited for Java, has been used as a starting point for the development of the OCL specifications. OCL is a more general language. Problems that have to be solved are, for instance, how to express in OCL the throwing of exceptions, how to test if a reference variable contains a null value, and how to handle the risk of overflow in the context of arithmetic integer operations. It has been shown that OCL lacks some important properties when it comes to specifying Java programs, but in other aspects is superior to JML.