// all API calls through '$' function/object
import $ from 'jquery';

// schedule a function to be called on load
$(function () { console.log('ready!'); });

// select all input elements in first form
const x = $('input', document.forms[0]);

// create new input elements with attributes
const y = $('<input>', { type: 'text' });

// create a resolved promise with a value

Promise.resolve(42)
  .then(console.log) // 42

Promise.resolve({ then: 42 })
  .then(console.log) // { then: 42 }

// create a promise with a "thenable"

Promise.resolve({ then: fulfill =>fulfill(42)})
  .then(console.log) // 42

• Static Type Checking
  • Dedicated syntax for expressing types
  • Limited Expressiveness
  • Static typing and subtyping rules
• Program Verification
  • Assertions written as boolean expressions
  • Disjunction, conjunction, negation, etc.
  • Subtyping is implication

function max(a, b) {
  requires(typeof(a)=="number");
  requires(typeof(b)=="number");
  ensures(result => result >= a);

  if (a > b) {
    return a;
  } else {
    return b;
  }
}
 

• Loops and recursion lead to unbound number of paths
• Inferring loop invariants and post-conditions undecidable
• Proposed Solution: Explicit code annotations for postconditions and invariants
  • Ensure decidable and predictable verification process

function sumTo (n) {
  requires(Number.isInteger(n));
  requires(n >= 0);
  ensures(res => res === (n + 1) * n / 2);

  let i = 0;
  let s = 0;
  while (i < n) {
    invariant(Number.isInteger(i));
    invariant(Number.isInteger(s));
    invariant(i <= n);
    invariant(s === (i + 1) * i / 2);
    i++;
    s = s + i;
  }
  return s;
}
        

function max(a, b) {
  requires(typeof(a)=="number");
  requires(typeof(b)=="number");
  ensures(result => result >= a);

  if (a > b) {
    return a;
  } else {
    return b;
  }
}

const x = max(23, 42);
assert(x >= 23);
 

• Higher-order Functions
  • Need syntax to describe function arguments
  • Introduces quantifiers into verification conditions
• Proposed Solution: spec syntax and bounded, trigger-based quantifier instantiation algorithm
  • Function calls act as explicit triggers for instantiation
  • Avoids brittle instantiation heuristics, matching loops and SMT solver timeouts
  • Ensure decidable and predictable verification process

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}
 

• $\{ call(x) \}$ is a trigger pattern
• $pre(\texttt{inc}, x)$ and $post(\texttt{inc}, x)$ uninterpreted function symbols
• $pre(\texttt{inc}, x)$ is satisfied by any integer value for $x$
• $post(\texttt{inc}, x)$ and precondition together imply $\texttt{inc}(x) > x$

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}
const y = inc(23);
assert(y > 23);
 

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}
const y = inc(23);
assert(y > 23);
 

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}

function twice (f, n) {
  requires(spec(f, (x)   => Number.isInteger(x),
                   (x,y) => Number.isInteger(y) && y > x));
  requires(Number.isInteger(n));
  ensures(res => res >= n + 2);
  return f(f(n));
}

const m = twice(inc, 3);
assert(m >= 5);
 

function f (g) {
  requires( spec(g,   x => x > 3,   (x, y) => y > 9));
  assert(   spec(g,   x => x > 4,   (x, y) => y > 8));
}
 

• The spec on g in the precondition satisfies the second, asserted spec
• This corresponds to co- and contravariance in function subtyping

• Nested recursive data structures (records, lists, trees)
• Proposed Solution: Simple immutable "classes" with invariants
  • Check invariant when creating instances
  • Instantiate invariant when accessing properties
  • Simple concept enables various applications
    • MergeSort algorithm, Promise API, Parameterized List

class Adder {
  constructor (base) { this.base = base; }
  invariant () { return Number.isInteger(this.base); }
  addTo (n) {
    requires(Number.isInteger(n));
    return this.base + n;
  }
}

function f (a) {
  requires(a instanceof Adder);
  ensures(res => res !== 2); // does not hold for "new A(-1)"
  return a.addTo(3);
}
 

• Pure functional core language with logical propositions as pre- and postconditions

• Verification rules similar to typing rules but also generate verification conditions
• Verification is sound:
  • Verified programs execute without getting stuck
• Verification algorithm is decidable
  • Decision procedure terminates for all inputs
• Complete mechanized proof in Lean

• Refinement types translate to annotations
  • Dependent function types translate to spec
• Conjuecture that well-typed programs translate to verifiable programs
  • Proof is work in progress

• Dafny
  • Verified programming language
  • Supports imperative programming with dynamic frames
  • Instantiation Heuristics can be unpredictable
  • Very limited higher-order functional programming
• LiquidHaskell
  • Refined Base Types and Dependent Function Types
  • Similar instantiation as esverify
• Decades of prior work on program verification

• Static verification for a dynamically-typed language
  • Annotate code with boolean expressions instead of types
  • Support for dynamically-typed idioms, e.g. Promise
  • Higher-order functional programming with spec
  • Comparable expressiveness to refinement type systems
• Bounded quantifier instantiation algorithm
  • Avoid brittle heuristics but requires explicit triggers
• Future work
  • Object-oriented and imperative programming
  • Interactive tools and Development Environments

1. Let $P$ be the verification condition
2. Let $n$ be the maximum level of quantifier nesting in $P$
3. Repeat $n$ times:
   1. Instantiate every universal quantifier in negative position in $P$ with every call trigger in negative position
   2. Lift all universal quantifiers in positive position to top level
4. Erase all quantifiers
5. Pass the quantifier-free formula to the SMT solver

function proof_f_mono (f, proof_f_inc, n, m) {
  // f is a function from non-negative int to int
  requires(spec(f,
      (x) => Number.isInteger(x) && x >= 0,
      (x, y) => Number.isInteger(y) && pure()));
  // proof_f_inc states that f is increasing
  requires(spec(proof_f_inc,
      x => Number.isInteger(x) && x >= 0,
      x => f(x) <= f(x + 1) && pure()));
  requires(Number.isInteger(n) && n >= 0);
  requires(Number.isInteger(m) && m >= 0);
  requires(n < m);
  // show that f is increasing for arbitrary n,m
  ensures(f(n) <= f(m));
  ensures(pure()); // no side effects
  proof_f_inc(n); // instantiate proof for n
  if (n + 1 < m) {
    // invoke induction hypothesis (I.H.)
    proof_f_mono(f, proof_f_inc, n + 1, m);
  }
}