Home Articles

“addFront”函数看起来非常程序化(即,不是声明性的)

Asked
Viewed 292 times
0

在Software Abstractions一书的第10页,它强调了Alloy的声明性质:

Alloy是声明性的,并通过比较before和after值来描述如何检查状态更改是否有效 .

第9页是添加新电子邮件地址簿的示例 . 该示例显示了“添加”之后的书籍状态与添加之前的书籍状态的不同之处 . 很好 - 确实很有说服力!

在页135上是参数化“列表”模块的示例 . 该示例具有“addFront”函数:

fun List.addFront (e: t): List {
    { p: List | p.next = this and p.element = e } }

这对我来说看起来不太具有说服力 . 要声明,我希望参数列表包含一个前后列表,我希望代码显示“addFront”之后的列表状态与“addFront”之前列表的状态有何不同(就像书的例子) .

为什么addFront以程序方式编写?是不是违反了合金的陈述性质?

1 Answer

  • 1

    声明意味着(对我来说),而不是解释计算如何逐步发生,你给出一个关于计算的观察 . 这就是这个函数的作用:它说如果你看一下addFront的结果,你会发现它的下一个字段包含输入列表,它的元素字段包含给定的元素 . 集合理解(结合规范化事实,在书中给出但未在此处显示)说“返回列表p使得......” .

    在这种情况下,对你来说似乎没有声明的是,Alloy看起来非常像你在函数式语言中使用的代码,例如ML . 但是在我看来,这些代码在本质上也是声明性的 - 实际上,由于这个原因,术语“声明性”已被广泛用于描述函数式语言 .

    我还应该注意,虽然Alloy确实是为支持声明性建模而设计的,而且我相信对于复杂的状态转换,声明式方法通常是最好的,我不会在这个问题上提前做出决定 . 模型中存在的问题是存在对行为没有意义的细节,但是由于建模语言的弱点而包括在内,或者因为建模者无意中引入了实现问题 .

Related