K-user mailing list

["Ayushi Rastogi" <rastogiayushi98 AT gmail.com>]

Respected Sir/Mam

While trying to implement string semantics whose snippet is as follows:

  syntax AExp  ::= Id |  String | AExp "$" AExp
                 | AExp "/" AExp              [left, strict]
                 > AExp "+" AExp              [left, strict]
  syntax Stmt ::= Id ":=" AExp
                         | "if"  BExp "then" Stmt "else" Stmt "end" "if" ";"
  syntax L::= String
  syntax Global ::= Id "," L
  syntax Par ::=  Global ": in Integer"
/* "$" is an operator that concatenates the string if and only if String S1 =/
= S2 and Glist is a list of Ids along with its string value*/
  rule <k> X:Id => S ...</k>
       <env>...   X |-> N ...</env>
       <store>... N  |-> S ...</store>
  rule S1 / S2 =>  S1 $ S2
  rule S1 + S2 => S1 $ S2
 rule <k> X:Id,S:L => S ...</k>
       <env>... X |-> N ...</env>
       <store>... N |-> S ...</store>
  rule  S1 $ S2 => S1 +String S2    when S1 =/=String S2
/* In following lines of code M is an identifier as the name of procedure just
like a variable that must be intialised with char P and acts like a program
counter for the called procedure*/
  rule <k> procedure M (Par) with SPARK_Mode is Block M ; =>. ...</k>
         <env>  M |-> N ... </env>
         <store>... N |->( P => String) ...</store>
  rule  X:Id:= R:AExp; => if notBool(X in Glist) then begin if X ==String (R $
M)
        then begin X := R $ M; end else halt; end if; end else begin if X
==String R
       +String M then begin end else halt; end if; end  end if;


and the error encountered as follows:

Unexpected sort AExp for term
_$_(#token(#KVariable,"R"),#token(#KVariable,"M")). Expected String.

I am not able to solve the problem as AExp is of kind sting and identifiers
then why operation $  cant be performed.

Detailed code can be seen on

http://www.kframework.org/tool/run/

in tutorial-> AdaSpark ->spar.k

Your worthy suggestions are most welcomed and express my gratitude for your
value that you have in helping me seek out a solution for same.

Thank you
Ayushi Rastogi