Suppose your favorite programming language does not support the notion of a set (i.e., set is not a built-in type) and I asked you to implement a set type in terms of the built-in types of your language, e.g., sequences (or arrays, more likely). This is a standard exercise in programming with data abstraction. For example, you might (1) represent sets in terms of sequences and then (2) implement each set operation in terms of operations on sequences and other built-in types. After you hand in your solution, I ask you to prove that your representation using sequences satisfies the abstract set type. How would you respond?
What we really care about is the relationship between a concrete state machine, C, and an abstract state machine, A:
where we usually read the arrow in one of many ways:
C satisfies A.
C implements A.
C is a refinement of A.
The program C is correct with respect to the specification A.
C and A can be interpreted in many ways:
C and A are both state machines.
C is a program and A is a specification.
C is an implementation and A is a specification.
C is a state machine and A is a predicate.
C and A are both programs.
C and A are both specifications.
C is an implementation and A is an interface specification.
C is a concrete data type and A is an abstract data type.
C is an Ada package body and A is a package specification.
C is a C function definition and A is a C function declaration.
C is a C++ class definition (implementation) and A is a class declaration (interface).
C is a high-level design and A is a set of customer's requirements.
C is a low-level design and A is a high-level design.
C is an implementation and A is a low-level design.