Java rewrite engine

:)

Spelling as in "spelling error": Euqal should be Equal.

Grigore


________________________________
From: Liyi Li [notifications@github.com]
Sent: Monday, November 10, 2014 11:45 AM
To: kframework/c-semantics
Subject: Re: [c-semantics] Java rewrite engine (#47)


In semantics/language/execution/stmt/goto.k:

> -          [structural]
> -
> -     rule <k> processGotoDown(gotoObject(TargetDepth:Int,
> -                    (ListItem(BlockNum:Int) BlockHist:List
> -               => searchInGotoObjectList(BlockHist, .List,
> -                    ActualHist, BlockHist)), _, _, _))
> -          ...</k>
> -          <nesting-depth> ActualDepth:Int </nesting-depth>
> -          <block-history> ActualHist:List </block-history>
> -          requires (TargetDepth =/=Int ActualDepth
> -               orBool BlockHist =/=K ActualHist)
> -               andBool (TargetDepth =/=Int ActualDepth +Int 1
> -               orBool ActualHist =/=K (ListItem(BlockNum) BlockHist))
> -          [structural]
> -
> +     syntax Bool ::= subListEuqalBack(List,List) [function]


What I mean here is that the boolean function is that the subListEquality function to check whether or not a list is contained in another list. "Back" indicates that the subListEquality is applied from the tail of a list.

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/c-semantics/pull/47/files#r20098447>.