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

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


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 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
>真(p_しません: bool): bool =
>  p_しません;
>しません(p_偽: bool): bool =
>  NOT (p_偽);
>END exampleJapanese

Attachment: patch-12.lisp
Description: patch-12.lisp