From 05fa5894f73ecd3779b11edd7e785d147a926e3d Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sat, 27 Jan 2024 17:43:26 +0900 Subject: [PATCH] Update README.md --- README.md | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/README.md b/README.md index afbb671..c8d26ad 100644 --- a/README.md +++ b/README.md @@ -86,3 +86,50 @@ If you want to run a manually built executable, run the following command instea ``` shell dune exec rethfl -- ``` + + +## Type Annotation (Experimenal Feature) +ReTHFL supports semi-automated verification via user specified refinement type annotations. + +### How to use + +Use options `--annot ` and `--target ` together with `--no-disprove`. +For example: + +``` +$ rethfl --no-disprove kmp.hfl --annot kmp.loop.annot --target toplevel +``` + +`CHECK_TARGET` must be one of the following: + +- `toplevel`: Checks whether the toplevel (i.e. the main) formula is valid under the assumption that the type annotation is correct. +- `annotation`: Checks whether the type annotation is correct. + +If ReTHFL returns valid for both `--target toplevel` and `--target annotation`, then it means the given formula is valid. +Since the *disprove mode is yet not implemented* for this semi-automated method, `--no-disprove` must be set. + +### Annotation file +Here is an exmalpe of an `.annot` file: +``` +%TYPE + +LOOP: + (plen: int -> + (slen: int -> + ((i: int -> ((int -> *) -> *[(0 <= i /\ i < plen)])) -> + ((i: int -> ((v: int -> *[(0 <= v + 1 /\ v + 1 < plen)]) -> *[(0 <= i /\ i < plen)])) -> + ((i: int -> ((int -> *) -> *[(0 <= i /\ i < slen)])) -> + (s: int -> + (p: int -> + ((int -> *) -> + *[0