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

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



Hi Ben,

What platform are you running on?  I tried with and without patches on
Linux 64 bit, and it always typechecks under SBCL.

Thanks,
Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> 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>
>