Início / coding / Perguntas / 78529388
Accepted
luomein
Asked: 2024-05-24 23:07:51 +0800 CST

O Alloy aceita variável livre?

  • 772

No livro Software Abstractions , capítulo 5.2.2 Skolemization, ele menciona, insira a descrição da imagem aqui

onde sxé uma nova variável livre e F[sx/x]é a restrição F, sxsubstituída por x.

Porém quando apresento a variável livre no Alloy, aparece erro de sintaxe. O Alloy aceita variável livre?

sig A {
  relation:  A
}
fact {
 some A
}
check{
  //correct expression
  //some a : A | one a.relation

  //Skolemization
  (a: A) and (one a.relation)
}
alloy

1 respostas

  1. Best Answer

    Primeiro, a Skolemização é uma operação lógica clássica e, se você ainda não a conhece, talvez seja uma boa ideia estudá-la usando um livro de lógica.

    Dito isto, a restrição mencionada no livro não é um código Alloy válido, é antes uma explicação do que acontece no nível do solucionador (o que Jackson chama de "restrição de análise"). Então não, escrito assim, o modelo Alloy não é válido devido à presença desta variável livre.

    Mas você não precisa realizar o Skolemization sozinho, pois o Alloy faz isso por você (dependendo da configuração no menu Opções).

    Ainda assim, se você quiser, você pode. A maneira de fazer isso é adicionar um novo objeto ado tipo Apara a variável existencial da seguinte forma:

    sig A {
  relation:  A
}
fact {
  some A
}
one sig a in A {}
check{ one a.relation }
    • 1

relate perguntas