TODO
*** Sandbox
- duplicate all core contracts to get rid of the inSandbox flag
*** Contracts
- Dependent Method Contract, see "this" in the pre and postcondition
- This-reference in Dependent Contract
*** Logger & Statistics
- On Callbacks
- Change Statistic flags
*** New Implicit Contract Conversion
*** Contracts
- Polymorphic
- Reflection (get/ set/ ..)
- ForAll
- Temporal Contract
- Disjunction/ Negation
*** Sandbox
- Integrate Pure.js, allow access to all pure elements, including calls of pure getter functions.
Benchmarks
==========
- Make inference and run with transparent proxies.
- Measure performance:
i) normal
ii) no-baseline
iii) no-ion
- Blank run with no-op Poxy
New Features
============
- Abstraction Contract
- Constructor applied to a value
- Temporal Contract
* Use proxies to build nice constructors that can be applied directly.
e.g.: Between(1,2); InstanceOf(Array);
# _
#| |__ _ _ __ _ ___
#| '_ \ || / _` (_-<
#|_.__/\_,_\__, /__/
# |___/
*** BUG in Spidermonkey Shell
- treat.decompile.js:77:21 TypeError: Function.prototype.toString called on incompatible object
- Function.prototype.toString can not be called on a function proxy
- Quick Fix works in LAX mode
*** Forall works only on Functions
*** Forall-contracts
* Implement lax/picky/indy semantics for forall-contracts
* Unpack contracted values
*** Exclude predefined contracts
isNaN overrides a global function in typedoctane
use an export function that exports all predefined contracts in
a special object (eg. contract(s) oder con)
## Features ##
* Object Contracts as Data Type Invariants
** Only testing lemmas
** Or If lemma than do
* Examples and security Properties
** Access one (A or B)/ Argument of a function
# __ __ _ _____ _
#| \/ |__ _ (_)___ _ _ |_ _|_ _ __| |__ ___
#| |\/| / _` || / _ \ '_| | |/ _` (_-< / /(_-<
#|_| |_\__,_|/ \___/_| |_|\__,_/__/_\_\/__/
# |__/
* Definition of Not/ Negation
- Previous version implemented for Not
# __ __ _ _____ _
#| \/ (_)_ _ ___ _ _ |_ _|_ _ __| |__ ___
#| |\/| | | ' \/ _ \ '_| | |/ _` (_-< / /(_-<
#|_| |_|_|_||_\___/_| |_|\__,_/__/_\_\/__/
*** White Listing for Sandboxes
- by an object
*** Summary of test cases
- merge test cases and use negative tests
*** Discuss the use cases of a Sandbox Constructor/ Sandbox Forall
- to produce \x.\y.C
*** Documentation and Webpage
*** replace all unnecessary checks by an debug check
*** make convenience contracts for all contracts using a constructor
# _____ _
#|_ _|__ __| |_ ___
# | |/ -_|_-< _(_-<
# |_|\___/__/\__/__/
*** Combination of Forall and Function Contracts
- Forall x.X->x *and* (Num->Num) -> (Num->Num)
*** Test run time difference of new version
- Flag for predicate evaluation
*** Deactivate contracts
- for example: \x.e @ C->C -> deactivate
- after return, all contracts on the input should be deactivated
- example from Lu; is there a use case
# ___ _ ___ _ _
#| __|__ __ _| |_ _ _ _ _ ___ | __|_ _| |_ ___ _ _ __(_)___ _ _ ___
#| _/ -_) _` | _| || | '_/ -_) | _|\ \ / _/ -_) ' \(_-< / _ \ ' \(_-<
#|_|\___\__,_|\__|\_,_|_| \___| |___/_\_\\__\___|_||_/__/_\___/_||_/__/
*** Lemma
- (cf. Haskell contracts)
- instead of asserting contracts to variables, defining a lemma with conditions.
*** Cast
- define a cast operator (C-D) v, that corresponds to ( \x.x @ C-D ) v
- is there a use case?
*** Subset Semantics
- define a relation C < D for contracts
*** Access Permission Contracts
- Include Access Contracts from JSConTest2
*** Temporal Contracts
- Specify the behavior of modules/functions in terms of temporal properties
- e.g. as a sequence of events,
- e.g. Access only allowed to property 'a' or property 'b', but not both at the same time
- e.g. A function is not allowed to be called again before it returns the from the first call
- e.g. access o.x; access o.y, return
- use temporal logic/ LTL
- use capabilities that allow to call a function