{"size": 1646, "ext": "scrbl", "max_stars_repo_path": "soft-contract/doc/main.scrbl", "max_stars_repo_name": "ralsei/soft-contract", "max_stars_repo_stars_event_min_datetime": "2015-01-15T01:16:57.000Z", "max_stars_repo_stars_event_max_datetime": "2022-03-15T22:41:56.000Z", "max_issues_repo_path": "soft-contract/doc/main.scrbl", "max_issues_repo_name": "camoy/soft-contract", "max_issues_repo_issues_event_min_datetime": "2015-01-08T04:23:43.000Z", "max_issues_repo_issues_event_max_datetime": "2021-10-30T05:49:35.000Z", "max_forks_repo_path": "soft-contract/doc/main.scrbl", "max_forks_repo_name": "camoy/soft-contract", "max_forks_repo_forks_event_min_datetime": "2018-02-22T22:11:32.000Z", "max_forks_repo_forks_event_max_datetime": "2021-11-10T22:00:31.000Z"}
{"max_stars_count": 30, "max_issues_count": 119, "max_forks_count": 7, "avg_line_length": 33.5918367347, "max_line_length": 81, "alphanum_fraction": 0.54981774}
#lang scribble/manual
@(require scriblib/figure)

@title{Soft Contract Verification}


@section{Installation}

@codeblock|{
raco pkg install soft-contract
}|


@section{Usage}

This collection implements a small functional language with contract verification
and counterexample generation.

You need to have Z3 in your path.
This program has been tested to work with Z3 4.3.2.

The demo currently supports the following subset of Racket:

@figure["Syntax" "Syntax"]{
@racketgrammar*[#:literals (module racket provide/contract define submod lambda
                             if cond else -> + - * / string-length number? real?
                             integer? boolean? false? cons? empty?
                             and/c or/c ->i)
                [program sub-module-form]
                [sub-module-form (module module-name racket
                                   (provide/contract provide-spec ...)
                                   (define id value) ...)]
                [provide-spec (id contract)]
                [require-spec (submod ".." module-name)]
                [value (lambda (id) expr) number boolean string symbol empty op]
                [expr id (if expr expr expr) (expr expr ...)
                      (cond [expr expr] ... [else expr])]
                [contract expr (or/c contract ...) (and/c contract ...)
                          (->i ([id contract] ...)
                               (id (id ...) contract))]
                [op + - * / string-length
                    number? real? integer? boolean? false? cons? empty?]]}


@section{Examples}

Example programs can be found under @bold{examples/}

