Scalarius: Concurrency macro – Project topics materials

Get Complete Project Material File(s) Now! »

Invariance

An invariant condition defines any state that does not change after initialization and thus is in-variant. In programming, this can be a shared field, for instance containing a network address frequently used amongst several methods or an external defined value required for a calculation. For fields that never change over the entire life time of a class instance, constants are the preferred way of defining these values. However, in some cases, it is required that a certain value may change but must remain unchanged. An invariant check actually performs an equality check if the supposed invariant field still equals its original value at a different time.
Thus, invariance checks fail if a supposed invariant field is 1) mutable and 2) its previous value has been unexpectedly modified later. Conversely, immutable fields are invariant by default and do not require additional checks. The importance of invariance checks is significantly higher in concurrency programming in order to prevent oblivious bugs triggered by several threads modifying a shared field simultaneously.
For instance, a commonly used invariant check is if a field after method execution still holds the same value as before method execution. This check detects unwanted modifications performed by other threads which usually happens if field access is not strictly ordered amongst threads [27][29].

Postcondition

A postcondition defines precisely what a method is expected to return. A postcondition can only be valid under the assumption of valid input according to its precondition. A postcondition only specifies what to return but not how to reach that goal. For instance, a method calculating a particular classification is expected to return one class for a particular range of the given parameter and another class for the remaining values. A precondition defines the total range of all valid input, for instance a numeric range from one to twelve. The postcondition on the other hand, defines what class must be assigned for certain values of the range. For instance, class A must be assigned to any value smaller or equal to six and class B to all others. The method body defines the actual calculation for the classification. If the actual calculation depends on an external value that may or may not change, an invariant check is applicable to ensure the correctness of the result.
In case of incorrect input, an error of the precondition is thrown whereas an incorrect implementation (that does wrong classification) throws an error triggered by the postcondition. Furthermore, if the assumed external field has changed during the computation, an invariant violation error is thrown. This detailed distinction separates different error sources which is a welcome help during debugging [27][29].

READ The tree-width of pseudoknotted RNAs is typically small

Liskov Substitution Principle

The Liskov substitution principle (LSP) is a definition of a sub-typing relation, called (strong) behavioural sub-typing, which is commonly applied in object-oriented programming languages. The principle was first introduced by Barbara Liskov in a 1987 conference keynote considering hierarchies in data abstraction [30]. In 1994, Liskov and Jeannette Wing [31] formulated the principle formally as:
Definition 3.1.1 (Liskov substitution principle). Let q(x) be a property provable about objects x of type T. Then q(y) should be provable for objects y of type S where S is a subtype of T (p. 2 in [31]).
In addition to type hierarchy, Liskov specifies three rules for inheritance of contracts. The first rule says that preconditions can only be weakened in subclasses. The second rule states that postconditions are only allowed to be strengthened in sub-classing. Third, invariants of the super type must be preserved in a subtype. Furthermore, a relevant concrete operation can be substituted for the corresponding operations of all its relevant ancestors (4.2 in [32]).

1 Introduction
2 Motivation
2.1 Question of research
2.2 Aim
3 Design by Contract
3.1 Overview
3.2 DBC in Eiffel
3.3 DBC in Java
3.4 DBC in Scala
3.5 DBC in ADA
3.6 Analysis
4 Scala
4.1 Overview
4.2 Scala syntax
4.3 Unified object mode
4.4 Scala type system
4.5 Implicits1
4.6 Class linearization
4.7 Modular mixin composition
4.8 Cake pattern
4.9 Functions
4.10 Functional composition
4.11 Scala concurrency
5 Results
6 f-DBC
7 CBR Case study
8 Empirical DBC usage
9 Scalarius: Concurrency macro
10 Discussion
11 Future work
A Appendix: The MIT License (MIT)
B Appendix: DBC usage script
C Appendix: CBR contract
Bibliography