Object-oriented Programming
What is Object Oriented Programming?
Object-oriented software construction is the building of software systems as structured collections of [...] abstract data type implementations.
Bertrand Meyer, “Object Oriented Software Construction”
Object Oriented Programming is about:
isolating clients from implementation details (abstraction)
isolating clients from the choice of data types (dynamic dispatching)
Object Oriented Programming is not:
the same as prototype programming (class and objects)
the same as scoping (class as the scope for methods)
the same as code reuse (use a component in a record in SPARK)
Prototypes and Scopes in SPARK
Types in SPARK come with methods aka primitive operations
Scope for the prototype is current declarative region
... or up to the first freezing point – point at which the type must be fully defined, e.g. when defining an object of the type
OOP without dynamic dispatching = Abstract Data Types
Classes in SPARK
Classes in SPARK are tagged records
Derived types are specializations of the root type
typically with more components
inheriting the methods on the parent type
can add their own methods
Methods in SPARK
Derived methods can be overriding or not
Method called depends on static type
Dynamic dispatching in SPARK
Class-wide types
type of object that triggers dispatching
method called depends on dynamic type
Class-wide views of objects
in Ada, usually manipulated through pointers
in SPARK, manipulated through parameter passing
A trivial example
what is called here?
The problems with dynamic dispatching
Control and data flow are not known statically
control flow – which subprogram is called when dispatching
data flow – what data this subprogram is accessing
similar to callbacks through subprogram pointers
Avionics standard DO-178C lists 3 verification options
run all tests on parent type where derived type is used instead
cover all possible methods at dispatching calls
prove type substitutability (Liskov Substitution Principle aka LSP)
LSP – the SPARK solution to dynamic dispatching problems
Class-wide contracts on methods
Pre'Class
specifies strongest precondition for the hierarchyPost'Class
specifies weakest postcondition for the hierarchy
Verification of dynamic dispatching calls
Class-wide contracts used for dynamic dispatching calls
LSP applies to data dependencies too
overriding method cannot read more global variables
overriding method cannot write more global variables
overriding method cannot have new input-output flows
SPARK RM defines
Global'Class
andDepends'Class
(not yet implemented ⟶ useGlobal
andDepends
instead)
Class-wide contracts and data abstraction
Abstraction can be used in class-wide contracts
Typically use expression functions for abstraction
Class-wide contracts, data abstraction and overriding
Abstraction functions can be overridden freely
overriding needs not be weaker or stronger than overridden
Inherited contract reinterpreted for derived class
Dynamic semantics of class-wide contracts
Class-wide precondition is the disjunction (or) of
own class-wide precondition, and
class-wide preconditions of all overridden methods
Class-wide postcondition is the conjunction (and) of
own class-wide postcondition, and
class-wide postconditions of all overridden methods
Plain
Post
+ class-widePre
/Post
can be used togetherProof guarantees no violation of contracts at runtime
LSP guarantees stronger than dynamic semantics
Redispatching and Extensions_Visible aspect
Redispatching is dispatching after class-wide conversion
formal parameter cannot be converted to class-wide type when
Extensions_Visible
isFalse
Aspect
Extensions_Visible
allows class-wide conversionparameter mode used also for hidden components
Code Examples / Pitfalls
Example #1
This code is not correct. Class-wide contracts are only allowed on tagged records.
Example #2
This code is not correct. Plain precondition on dispatching subprogram is not allowed in SPARK. Otherwise it would have to be both weaker and stronger than the class-wide precondition (because they are both checked dynamically on both plain calls and dispatching calls).
Plain postcondition is allowed, and should be stronger than class-wide postcondition (plain postcondition used for plain calls).
Example #3
This code is correct. Class-wide precondition of Int.Bump
is inherited
by Approx_Int.Bump
. Class-wide postcondition of Approx_Int.Bump
is
stronger than the one of Int.Bump
.
Example #4
This code is not correct. A type must be declared abstract or "+"
overridden.
Example #5
This code is not correct. A type must be declared abstract or Reset
overridden Reset
is subject to Extensions_Visible
False
.
Example #6
This code is not correct. High: extension of Arg
is not initialized in
Reset
.
Example #7
This code is correct. Redispatching ensures that Arg
is fully
initialized on return.
Example #8
This code is correct. State automaton encoded in class-wide contracts is respected.
Example #9
This code is not correct. Medium: class-wide precondition might be stronger than overridden one
Example #10
This code is correct. Predicate encodes the additional constraint on opened files. Type invariants are not yet supported on tagged types in SPARK.