Perfect supports this kind of abstraction in specifications as well as implementations. Although it is sometimes possible to define a class adequately by its behaviour alone, more often it is necessary to have some model of the data stored by the class in order to understand what the class is for. The class methods are specified in terms of this abstract data model (although naturally, clients of the class do not have direct access to it). This leaves the way open to refining the abstract data model to a more efficient implementation model.
This source of confusion can lead to unexpected results. For example, if two variables X and Y both refer to the same object, then if a member method is called on X to update the object, the change will also be visible to Y. Sometimes this is exactly what we want; but it is also a frequent source of error.
A post-assertion is a declaration of some condition that must hold when a method or constructor completes. (Some authors would call this a postcondition, but we have a stronger meaning for that term. See below for the differences.)
In Perfect, constructors are declared using the keyword build. The parameter list is enclosed in curly brackets to reflect the syntax of a constructor call. You never omit "{}" even if the constructor parameter list is empty.
Constructors have no side-effects, so changeable parameters are not permitted.
Constructors may have preconditions, but constructor preconditions cannot refer to the current object, because there isn't one at the start of the call. It follows that a constructor which takes no parameters cannot have a meaningful precondition.
For example, suppose you declared BankAccount and then SavingsAccount, but in declaring SavingsAccount you redefined the inherited method withdraw. This gives you two versions of withdraw. Then, each time a call is made to myAccount.withdraw(someMoney), the version of withdraw that is called will depend on whether myAccount holds a plain BankAccount, or a SavingsAccount.
The idea is that data belonging to an object is under the control of the methods (also known as functions) of that object, and may not be accessed in any way other than by those methods. The implementation details of the methods are not generally known.
What is generally known is what each method does, and the prototype for each method. So the developer using a method knows what parameters to pass to it, and what sort of result will be returned, and any side-effects that it may have.
The developer does not know, and does not need to know, how the method achieves its purpose. The data belonging to each object is only accessible by using these methods - hence it is "encapsulated".
This is not about haunted houses!
A ghost (whatever) in Perfect is one which has no executable code.
Perfect allows ghost methods, ghost operators, ghost selectors, and ghost schemas.
So what good is something with no executable code, then? Well, for
instance, when defining functions to represent abstract properties, it
sometimes happens that the property is only used in declaring preconditions,
postconditions, class invariants, etc.
Side effects are sometimes used deliberately; but are better avoided if possible, as they can make a program harder to understand. In Perfect, functions and constructors may not have side-effects.
Validation means checking that the specification of the software system under development conforms with the user's requirements.
Verification, on the other hand, means checking that the system performs in accordance with its (valid) specification.
Perfect Developer can validate your specification (provided that you
correctly ascertained and expressed the user's requirements) and can verify
that the implementation will conform to the specification.
System-level testing is normally still needed to ensure there were no
requirements-gathering errors at the beginning of the development process and
no hardware or back-end compiler bugs at the other end.
Unit-level testing is normally regarded as unnecessary
when implementations are mathematically
validated against specifications and requirements.