이 합금 코드의 문제점은 무엇입니까?

아래 코드에 대한 구문 오류 메시지가 나타납니다. 메시지는 addLocal 어설 션에서 표시된 위치를 지정합니다. "30 번째 줄의 구문 오류 9 : 여기에 나타날 수있는 토큰은 1 개입니다.)" 여기서 잘못된 점을 볼 수 없습니다. 합금의 구문을 사용하여 (또는 허용) 변경 어떤 점에서이 합금 코드의 문제점은 무엇입니까?

나는 결코 확실히 이해 이유로

abstract sig Target{} 

sig Addr extends Target{} 
sig Name extends Target{} 

sig Book 
{ 
    addr: Name->Target 
} 

pred add(b, b1:Book, n:Name, t:Target) 
{ 
    b1.addr = b.addr + (n->t) 
} 

fun lookup (b: Book, n: Name): set Addr 
{ 
    n.^(b.addr) & Addr 
} 

assert addLocal 
{ 
    all 
     b,b1:Book, 
     n,n1:Name, 
     t:Target | 
      add(b, b1, n, t) and n != n1 => lookup(b, n1) = lookup(b1, n1) 
      // |- error position 
}

출처

2015-01-15 Attila Karoly

는 대괄호를 필요로, 술어와 함수의 인자 주위에 괄호.

add[b, b1, n, t] and n != n1 => lookup[b, n1] = lookup[b1, n1]

내가 확실하게 내 머리에 단단히 충분히 문법을 가지고 있지 않지만, 소프트웨어 추상화의 부록 B의 문법에 잠깐 눈 : 그래서 addLocal의 해당 줄을 다시 구두점해야은 괄호가 술어 선언에서 인수를 감쌀 수 있지만 술어 참조에서는 감쌀 수는 없다고 제안합니다. 표현식 위치에서 괄호는 항상 단일 표현식을 감싸므로 인수 목록에서 첫 번째 쉼표를 발견 할 때 구문 분석기가 중지되는 이유를 설명합니다.

출처

2015-01-15 15:08:01

답변 해 주셔서 감사합니다. –

나는 대괄호가 선언에서도 받아 들여지고 있음을 발견했다 :'pred add [b, b1 : Book, n : Name, t : Target] {}' –

이 합금 코드의 문제점은 무엇입니까?

답변

관련 문제