我想通过使用来自 KFramework 的 SIMPLE 的以下代码来实现多维列表
module ARRAYST-SYNTAX
imports DOMAINS-SYNTAX
syntax Id ::= "main" [token]
syntax TypeName ::= AType | BType
syntax AType ::= "INT"
syntax BType ::= "ARRAY" "[" Exps "]" "OF" TypeName
syntax Stmt ::= "var" Exps ";"
| Id ":" "ARRAY" "[" Exps "]" "OF" TypeName ";"
syntax Exp ::= Val | Id
| "(" Exp ")" [bracket]
| "++" Exp
> Exp "[" Exps "]" [strict]
> Exp "(" Exps ")" [strict]
| "-" Exp [strict]
| "sizeOf" "(" Exp ")" [strict]
| "read" "(" ")"
> left:
Exp "*" Exp [strict, left]
| Exp "/" Exp [strict, left]
| Exp "%" Exp [strict, left]
> left:
Exp "+" Exp [strict, left]
| Exp "-" Exp [strict, left]
> non-assoc:
Exp "<" Exp [strict, non-assoc]
| Exp "<=" Exp [strict, non-assoc]
| Exp ">" Exp [strict, non-assoc]
| Exp ">=" Exp [strict, non-assoc]
| Exp "==" Exp [strict, non-assoc]
| Exp "!=" Exp [strict, non-assoc]
> "!" Exp [strict]
> left:
Exp "&&" Exp [strict(1), left]
| Exp "||" Exp [strict(1), left]
> "spawn" Block
> Exp "=" Exp [strict(2), right]
> Exp ".." Exp [strict]
syntax Ids ::= List{Id,","}
syntax Exps ::= List{Exp,","} [strict] // automatically hybrid now
syntax Val ::= Int | Bool | String
| array (TypeName, Int, Int, Int)
syntax Block ::= "{" "}"
| "{" Stmt "}"
syntax Stmt ::= Block
| Exp ";" [strict]
| "if" "(" Exp ")" Block "else" Block [avoid, strict(1)]
| "if" "(" Exp ")" Block
| "while" "(" Exp ")" Block
| "for" "(" Stmt Exp ";" Exp ")" Block
syntax Stmt ::= Stmt Stmt [right]
rule if (E) S => if (E) S else {} [macro]
rule for(Start Cond; Step) {S} => {Start while (Cond) {S Step;}} [macro]
rule for(Start Cond; Step) {} => {Start while (Cond) {Step;}} [macro]
rule var E1:Exp, E2:Exp, Es:Exps; => var E1; var E2, Es; [macro-rec]
rule var X:Id = E; => var X; X = E; [macro]
endmodule
module ARRAYST
imports ARRAYST-SYNTAX
imports DOMAINS
syntax KResult ::= Val
configuration <T color="red">
<k color="green"> $PGM:Stmt</k>
<env color="violet"> .Map </env>
<store color="white"> .Map </store>
<nextLoc color="gray"> 0 </nextLoc>
</T>
syntax KItem ::= "undefined" [latex(\bot)]
rule <k> var X:Id; => . ...</k>
<env> Env => Env[X <- L] </env>
<store>... .Map => L |-> undefined ...</store>
<nextLoc> L => L +Int 1 </nextLoc>
context var _:Id[HOLE];
rule <k> X:Id : ARRAY [I1:Int .. I2:Int] OF At:AType; => . ...</k>
<env> Env => Env[X <- L] </env>
<store> ... .Map => L |-> array(At, L +Int 1, I2 -Int I1 +Int 1, I1)
(L +Int 1) ... (L +Int I2 -Int I1 +Int 1) |-> undefined ...</store>
<nextLoc> L => L +Int 1 +Int I2 -Int I1 +Int 1 </nextLoc>
requires I2 -Int I1 +Int 1 >=Int 0 [structural]
syntax Id ::= "$1" | "$2"
rule X:Id : ARRAY [I1:Int .. I2:Int, I3:Int .. I4:Int, Es:Exps] OF At:AType;
=> X:Id : ARRAY [I1:Int .. I2:Int] OF At:AType;
{
for(var $1 = I1; $1 <= I2; $1 = $1 + 1) {
$2 : ARRAY [I3 .. I4, Es] OF At;
X[$1] = $2; //It can't work well, but if I use X[Int], it can work
}
} [structural]
rule <k> X:Id => V ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
rule I1 + I2 => I1 +Int I2
rule I1 - I2 => I1 -Int I2
rule I1 * I2 => I1 *Int I2
rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0
rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0
rule - I => 0 -Int I
rule I1 < I2 => I1 <Int I2
rule I1 <= I2 => I1 <=Int I2
rule I1 > I2 => I1 >Int I2
rule I1 >= I2 => I1 >=Int I2
rule ! T => notBool(T)
rule true && E => E
rule false && _ => false
rule true || _ => true
rule false || E => E
rule V:Val[N1:Int, N2:Int, Es:Exps] => V[N1][N2, Es] [structural, anywhere]
rule array(_, L, _, I)[N:Int] => lookup(L +Int N -Int I) requires N >=Int I [structural, anywhere]
rule sizeOf(array(_,_,N,_)) => N
context (HOLE => lvalue(HOLE)) = _
rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (_ => V) ...</store> [assignment]
rule {} => . [structural]
rule <k> { S } => S ...</k> [structural]
rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
rule _:Val; => .
rule if (true) S else _ => S
rule if (false) _ else S => S
rule while (E) S => if (E) {S while(E)S} [structural]
syntax Exp ::= lookup(Int)
rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [lookup]
// For parsing reasons, we prefer to allow lvalue to take a K
syntax Exp ::= lvalue(K)
syntax Val ::= loc(Int)
// Local variable
rule <k> lvalue(X:Id => loc(L)) ...</k> <env>... X |-> L:Int ...</env> [structural]
// Array element: evaluate the array and its index;
// then the array lookup rule above applies.
context lvalue(_::Exp[HOLE::Exps])
context lvalue(HOLE::Exp[_::Exps])
// Finally, return the address of the desired object member
rule lvalue(lookup(L:Int) => loc(L)) [structural]
syntax Map ::= Int "..." Int "|->" K [function, latex({#1}\ldots{#2}\mapsto{#3})]
rule N...M |-> _ => .Map requires N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
endmodule
但是当我运行程序时它不能很好地工作：
a1 : ARRAY [4..5,3..7] OF INT;
显示 在这里输入图片描述 我发现它无法处理X[$1]，但是它知道如何处理X[4]，这意味着$1不能更改为4。我不知道原因以及如何处理。
