Что не так с этим кодом Alloy?

Я получаю сообщение об ошибке синтаксиса для кода ниже. Сообщение обозначает отмеченную позицию в утверждении 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   
}

alloy
person Attila Karoly    schedule 15.01.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

По причинам, которые я так и не понял, в какой-то момент синтаксис Alloy изменился с использования (или разрешения) круглых скобок вокруг аргументов предикатов и функций на требование квадратных скобок. Таким образом, соответствующая строка addLocal должна быть повторно пунктуирована:

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

У меня недостаточно прочная грамматика в голове, чтобы быть уверенным, но беглый взгляд на грамматику в приложении B к Абстракциям программного обеспечения показывает, что круглые скобки могут заключать аргументы в объявлении предиката, но не в предикатной ссылке; в позиции выражения круглые скобки всегда обрамляют одно выражение, что объясняет, почему синтаксический анализатор останавливается, когда встречает первую запятую в списке аргументов.

person C. M. Sperberg-McQueen    schedule 15.01.2015
comment
Большое спасибо за ваши ответы. - person Attila Karoly; 15.01.2015
comment
Я только что заметил, что квадратные скобки также принимаются в объявлениях: pred add [b, b1: Book, n: Name, t: Target] {} - person Attila Karoly; 15.01.2015