[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Interpreting of "ん" as "±" (or something else?)



I cloned the NASA PVS Library and configured my environment to use it, but I still get that same problem. Does the solution possibly rely on the very latest PVS from GitHub as well?

I am using 6.0, and have just cloned the PVS repository itself, as long as SBCL, but got stuck:
  • I did figure out that I needed to run autoconf
  • I also then figured out that my PVSPATH variable needs to end with a trailing “/“
  • building SBCL depended on having SBCL (or another LISP) already built

I’ll eventually figure out how to build PVS, but just thought I’d let you know that with the default 6.0 PVS and the GitHub NASA libraries the problem persisted for me (on Mac OS X, if that’s relevant).

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




On Jul 10, 2015, at 9:58 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:

Ben,

This theory type-checks without problem using the patches in the github
version of the NASA PVS Library. Sam recently added the attached patch,
which may have solved the problem.

Cesar 
-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 7/10/15 3:31 AM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
on behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

exampleJapanese: THEORY
BEGIN

真(p_しません: bool): bool =
p_しません;

しません(p_偽: bool): bool =
NOT (p_偽);

END exampleJapanese


<patch-12.lisp>