Smart cards are small-embedded devices with strong security requirements.
To fulfill those requirements, formal methods appear as promising techniques. The B method has already been used to model smart card components. However, smart cards have also very strong programming constraints, for both memory usage and computing power. Currently the code generated from a B specification does not meet those constraints. This paper presents some classical optimisation techniques that are well suited for B specifications, and that need to be included within a code generator to embed this generated code.