Predicates/ghost functions for higher-order annotations

levjj / esverify

ECMAScript verification with SMT solvers

https://esverify.org/

MIT License

123 stars 5 forks source link

Predicates/ghost functions for higher-order annotations #27

Open levjj opened 5 years ago

levjj commented 5 years ago

There is already adhoc support for higher-order annotations by using spec with verification-only functions. However, this should become a core langauge feature to provide better support for parametric polymorphism, etc.