Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/parsers/parser_lustre.mly
81 81
%token INVARIANT MODE CCODE MATLAB
82 82
%token EXISTS FORALL
83 83
%token PROTOTYPE LIB
84
%token BY
85
%token <int> KINDUCTION
84 86
%token EOF
85 87

  
86 88
%nonassoc p_string
......
370 372
    nd
371 373
  }
372 374

  
375
proof_annotation:
376
| BY k=KINDUCTION { Kinduction k }
377

  
373 378
contract_content:
374 379
| { empty_contract }
375 380
/* | CONTRACT cc=contract_content */
......
380 385
  { merge_contracts (mk_contract_var x false (Some (mktyp $sloc t)) e $sloc) cc }
381 386
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content
382 387
  { merge_contracts (mk_contract_assume x e) cc }
383
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content
384
  { merge_contracts (mk_contract_guarantees x e) cc }
388
| GUARANTEES x=ioption(STRING) e=qexpr p=proof_annotation? SCOL cc=contract_content
389
  { merge_contracts (mk_contract_guarantees x e p) cc }
385 390
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content
386 391
  { merge_contracts (
387 392
        let r, e = mc in

Also available in: Unified diff