tchajed

method sum_seq(xs: seq<int>) returns (z:int) {
    var sum := 0;
    var i := 0;
    while i < |xs|
        invariant i <= |xs|
    {
        sum := sum + xs[i];
        i := i + 1;
    }
    return sum;

tchajed

#!/bin/bash

info() {
  echo -e "\033[34m$1\033[0m"
}

error() {
  echo -e "\033[31m$1\033[0m"
}

tchajed

#!/usr/bin/env bash

# iris-release.sh prepares a commit for https://github.com/coq/opam to
# add a new version of std++ and Iris to the Coq opam repository.
#
# Requires a clone of opam-coq-archive. The opam files from std++ and Iris are
# retrieved by downloading their releases by tag.

set -eu

tchajed

#!/bin/sh

dafny verify --solver-log example.smt2 --boogie /normalizeNames:0 example.dfy

tchajed

#!/bin/sh

verus --log-smt example.rs
# output is in .verus-log/root.smt2