Này được sử dụng cho thông tin được tạo ra khi đối tượng thay đổi trạng thái, ví dụ, một dấu vân tay chứng chỉ (băm Giấy chứng nhận đã được mã hóa) chỉ tồn tại một khi giấy chứng nhận đã được ký kết và đang trong trạng thái cao. | 172 5 Verification of the cryptlib Kernel to be maintained and updated once the initial implementation has been completed. This is particularly critical when the implementation is subject to constant revision and change but has the downside that implementation languages don t as a rule make terribly good specification languages. Using this approach ties in to the concept of cognitive fit matching the tools and techniques that are used to the task to be accomplished 35 36 . If we can perform this matching we can assist in the creation of a consistent mental representation of the problem and its solution. In contrast if a mismatch between the representation and the solution occurs then the person examining the code has to first transform it into a fitting representation before applying it to the task at hand or alternatively formulate a mental representation based on the task and then try and work backwards to the actual representation. By matching the formal representation to the representation of the implementation we can avoid this unnecessary error-prone and typically very labour-intensive step. The next logical step below the formal specification then becomes the ultimate specification of the real system the source code that describes every detail of the implementation and the one from which the executable system is generated. Ensuring a close match between the specification and implementation raises the spectre of implementation bias in which the specification unduly influences the final implementation. For example one source comments that A specification should describe only what is required of the system and not how it is achieved . There is no reason to include a how in a specification specifications should describe what is desired and no more 37 . Empirical studies of the effects of the choice of specification language on the final implementation have shown that the specification language s syntax semantics and representation style can heavily influence the
