Skip to content

Commit

Permalink
Added oldValue support to @ensures (#167)
Browse files Browse the repository at this point in the history
  • Loading branch information
mlhaufe authored Dec 10, 2020
1 parent 2ab7416 commit 63e9569
Show file tree
Hide file tree
Showing 8 changed files with 116 additions and 27 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
* Linting fixes
* Updated contact info in README and package.json
* BREAKING CHANGE: Decorators now accept arrow functions instead of traditional functions. The first parameter is `self`.
* BREAKING CHANGE: @ensures now provides `old` as a parameter to access instance property values before feature execution

## v0.18.1

Expand Down
60 changes: 43 additions & 17 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -367,7 +367,9 @@ The precondition of `Sub.prototype.method` is:

## Ensures

The @ensures decorator describes and enforces an assertion that must be true after its associated feature has executed. In other words after a client of your class has executed a method or accessor the defined postcondition must be met or an error [will be raised](#the-order-of-assertions).
The `@ensures` decorator describes and enforces an assertion that must be true after its associated feature has executed.
In other words after a client of your class has executed a method or accessor the defined postcondition must be met or an
error [will be raised](#the-order-of-assertions).

```typescript
@invariant
Expand All @@ -380,13 +382,34 @@ class Stack<T> {
}
```

In the above example the postcondition of executing push on a stack is that it is not empty. If this assertion fails an AssertionError is raised.
In the above example the postcondition of executing push on a stack is that it is not empty. If this assertion fails an `AssertionError` is raised.

An @invariant decorator must also be defined either on the current class or on an ancestor as shown in the example.
An `@invariant` decorator must also be defined either on the current class or on an ancestor as shown in the example.

Static features, including the constructor, can not be assigned an @ensures decorator. In the future this may be enabled for non-constructor static methods but the implications are not clear at present.
Static features, including the constructor, can not be assigned an `@ensures` decorator. In the future this may be enabled for non-constructor static methods but the implications are not clear at present.

If a class feature is overridden then the @ensures assertion still applies:
In addition to the `self` argument there is also an `old` argument which provides access to the properties of the instance before its associated member was executed.

```typescript
@invariant
class Stack<T> {
...
@ensures<Stack<T>>((self,old) => self.size == old.size + 1)
push(value: T) {
this.#implementation.push(value);
}

@ensures<Stack<T>>((self,old) => self.size == old.size - 1)
pop(): T {
return this.#implementation.pop();
}
}
```

Only public properties can be accessed via `old`. This restriction is to prevent infinite recursion through existing assertions.
Also due to a limitation in the current version of JavaScript, decorators are not able to access private properties directly (`#foo`).

If a class feature is overridden then the `@ensures` assertion still applies:

```typescript
class MyStack<T> extends Stack<T> {
Expand All @@ -401,18 +424,24 @@ myStack.push()
myStack.isEmpty() == false;
```

If a class feature with an associated @ensures is overridden, then the new feature can have an @ensures declaration of its own. This postcondition can not weaken the postcondition of the original feature. The new postcondition will be and-ed with it's ancestors. If all are true, then the obligation is considered fulfilled by the user of the feature, otherwise an AssertionError is raised.
The remaining arguments of `@ensures` reflect the arguments of the associated feature.

```typescript
@invariant
class Base {
@ensures((_,x: number) => 0 <= x && x <= 10)
@ensures((_self,_old,x: number) => 0 <= x && x <= 10)
method(x: number) { ... }
}
```

If the class feature with an associated `@ensures` is overridden, then the new feature can have an `@ensures` declaration of its own.
This postcondition can not weaken the postcondition of the original feature. The new postcondition will be and-ed with it's ancestors.
If all are true, then the obligation is considered fulfilled by the user of the feature, otherwise an `AssertionError` is raised.

```typescript
class Sub extends Base {
@override
@ensures((_,x: number) => -10 <= x && x <= 20)
@ensures((_self,_old,x: number) => -10 <= x && x <= 20)
method(x: number) { ... }
}
```
Expand All @@ -421,23 +450,20 @@ In the above example the postcondition of Sub.prototype.method is:

`(-10 <= x && x <= 20) && (0 <= x && x <= 10)`

The `_` parameter is a placeholder for the unused self reference.

Multiple @ensures can be declared for a feature. Doing so will require that all of these are true after the associated feature has executed:
Multiple `@ensures` can be declared for a feature. Doing so will require that all of these are true after the associated feature has executed:

```typescript
@invariant
class Base {
@ensures((_,x: number) => 0 <= x && x <= 10)
@ensures((_,x: number) => x % 2 == 0)
method(x: number) {
... }
@ensures((_self,_old,x: number) => 0 <= x && x <= 10)
@ensures((_self,_old,x: number) => x % 2 == 0)
method(x: number) { ... }
}

class Sub extends Base {
@override
@ensures((_,x: number) => -10 <= x && x <= 20)
@ensures((_,x: number) => Number.isInteger(x))
@ensures((_self,_old,x: number) => -10 <= x && x <= 20)
@ensures((_self,_old,x: number) => Number.isInteger(x))
method(x: number) { ... }
}
```
Expand Down
50 changes: 45 additions & 5 deletions src/EnsuresDecorator.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ describe('Preconditions cannot be weakened in a subtype', () => {

@invariant
class Base {
@ensures((_, value: number) => 10 <= value && value <= 30)
@ensures((_self, _old, value: number) => 10 <= value && value <= 30)
method(value: number): number { return value; }
}

Expand All @@ -232,7 +232,7 @@ describe('Preconditions cannot be weakened in a subtype', () => {

class Weaker extends Base {
@override
@ensures((_, value: number) => 1 <= value && value <= 50)
@ensures((_self, _old, value: number) => 1 <= value && value <= 50)
method(value: number): number { return value; }
}

Expand All @@ -247,7 +247,7 @@ describe('Preconditions cannot be weakened in a subtype', () => {

class Stronger extends Base {
@override
@ensures((_, value: number) => 15 <= value && value <= 20)
@ensures((_self, _old, value: number) => 15 <= value && value <= 20)
method(value: number): number { return value; }
}

Expand All @@ -270,7 +270,7 @@ describe('A class feature with a decorator must not be functional until the @inv

@invariant
class Okay {
@ensures((_, value: number) => 10 <= value && value <= 30)
@ensures((_self, _old, value: number) => 10 <= value && value <= 30)
method(value: number): number { return value; }
}

Expand All @@ -281,7 +281,7 @@ describe('A class feature with a decorator must not be functional until the @inv
});

class Fail {
@ensures((_, value: number) => 10 <= value && value <= 30)
@ensures((_self, _old, value: number) => 10 <= value && value <= 30)
method(value: number): number { return value; }
}

Expand All @@ -290,4 +290,44 @@ describe('A class feature with a decorator must not be functional until the @inv

expect(() => fail.method(15)).toThrow(MSG_INVARIANT_REQUIRED);
});
});

/**
* https://github.com/final-hill/decorator-contracts/issues/98
*/
describe('The @ensures decorator has access to the properties of the instance class before its associated member was executed', () => {
const {invariant, ensures} = new Contracts(true);

test('Stack Size', () => {
@invariant
class Stack<T> {
#implementation: T[] = [];
_size = 0;

@ensures<Stack<T>>((self,old) => self._size == old._size - 1)
pop(): T {
const result = this.#implementation.pop()!;
this._size = this.#implementation.length;

return result;
}

@ensures<Stack<T>>((self,old) => self._size == old._size + 1)
push(item: T): void {
this.#implementation.push(item);
this._size = this.#implementation.length;
}
}

const stack = new Stack<string>();

expect(stack._size).toEqual(0);
expect(() => {
stack.push('a');
stack.push('b');
stack.push('c');
}).not.toThrow();
expect(() => stack.pop()).not.toThrow();
expect(stack._size).toEqual(2);
});
});
4 changes: 2 additions & 2 deletions src/EnsuresDecorator.ts
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@
*/

import MemberDecorator from './MemberDecorator';
import { PredicateType } from './typings/PredicateType';
import DescriptorWrapper from './lib/DescriptorWrapper';
import Assertion from './Assertion';
import { MSG_INVALID_DECORATOR, MSG_NO_STATIC } from './Messages';
import { EnsuresType } from './typings/EnsuresType';

/**
* The `@ensures` decorator is an assertion of a postcondition.
Expand All @@ -34,7 +34,7 @@ export default class EnsuresDecorator extends MemberDecorator {
* @returns {MethodDecorator} - The method decorator
* @throws {AssertionError} - Throws an AssertionError if the predicate is not a function
*/
ensures<S extends object>(predicate: PredicateType<S>): MethodDecorator {
ensures<S extends object>(predicate: EnsuresType<S>): MethodDecorator {
const checkMode = this.checkMode,
assert: Assertion['assert'] = this._assert;
this._checkedAssert(typeof predicate == 'function', MSG_INVALID_DECORATOR);
Expand Down
11 changes: 10 additions & 1 deletion src/MemberDecorator.ts
Original file line number Diff line number Diff line change
Expand Up @@ -187,14 +187,23 @@ export default abstract class MemberDecorator {
);
}

const old = Object.entries(this).reduce((acc,[key,value]) => {
if(typeof value != 'function') {
Object.defineProperty(acc,key,{value});
}

return acc;
}, Object.create(null));

let result;

try {
result = feature.apply(this, args);
if(allEnsures.length > 0) {
checkedAssert(
allEnsures.every(
ensures => ensures.every(
ensure => ensure.call(this, this, ...args)
ensure => ensure.call(this, this, old, ...args)
)
),
ensuresError
Expand Down
2 changes: 1 addition & 1 deletion src/RescueDecorator.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -420,7 +420,7 @@ describe('If an error is thrown in @demands, the error is raised to the caller',
@rescue((_, _error, args: any[], _retry) => {
if(args[0] === -2) { throw new Error('Rescue Error'); }
})
@demands((_,value: number) => value >= 0)
@demands((_, value: number) => value >= 0)
method(value: number): void {
this.#value = value;
}
Expand Down
3 changes: 2 additions & 1 deletion src/lib/FeatureRegistry.ts
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,14 @@
import DescriptorWrapper from './DescriptorWrapper';
import { PredicateType } from '../typings/PredicateType';
import { RescueType } from '../typings/RescueType';
import { EnsuresType } from 'typings/EnsuresType';

export const DECORATOR_REGISTRY = Symbol('Decorator Registry');

export class FeatureRegistration {
readonly demands: PredicateType<any>[] = [];
descriptorWrapper: DescriptorWrapper;
readonly ensures: PredicateType<any>[] = [];
readonly ensures: EnsuresType<any>[] = [];
overrides = false;
rescue: RescueType<any> | undefined;

Expand Down
12 changes: 12 additions & 0 deletions src/typings/EnsuresType.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
/*!
* @license
* Copyright (C) 2020 Michael L Haufe
* SPDX-License-Identifier: AGPL-3.0-only
* @see <https://spdx.org/licenses/AGPL-3.0-only.html>
*/


type NonFunctionPropertyNames<T> = { [K in keyof T]: T[K] extends Function ? never : K }[keyof T];
type Properties<T> = Pick<T, NonFunctionPropertyNames<T>>;

export type EnsuresType<S extends object> = (self: S, old: Properties<S>, ...args: any[]) => boolean;

0 comments on commit 63e9569

Please sign in to comment.