PVS

PVS copied to clipboard

Just to record it on github: ``` a: theory begin t : type t2 : type interface : [ t -> setof[t2]] end a b: theory begin t2 : type...

disteph

In the presence of a datatype declaration in the root theory (argument theoryref in the unusedby-proofs-of-formulas LISP function) the assertion (assert th) in the unused-by-proofs-of LISP function fails. An simple...

dMaggot

The type language---records in particular

3

I am writing something mainly for myself on transliterating Z to PVS. (I know...I'm mad...) At one point what I WANT to write is (using _ to mimic the priming...

stever00

commit: 182c18 Build system: i386-apple-darwin17.7.0 SBCL: 1.4.11.68-9456dfc60 I've run `autoconf`, `./configure` and `make`. I get the following error. I pressed "1" to ignore the error and continue. That looks to...

holtzermann17

Implement a Dynamic Tree View

1

We need a dynamic tree visualization API with the following capabilities: - Expand/Collapse nodes - Add/Remove nodes - Change node colors/data - Zoom in/out - Context menu for nodes

happyhuman

"pvs-gui.json" still requires the schema for the error objects.

happyhuman

I built from source (a2940953d4f3c3abbf43799875e28e4044ddc424), and when I open the pvs emacs build I get this: ``` Debugger entered--Lisp error: (file-missing "Cannot open load file" "No such file or directory"...

quinn-dougherty