1

在 VDM-SL 中指定隐式函数时，是否可以指定柯里化函数？下面的 test1 和 test2 是显式的 uncurried 和 curried 函数，而 test3 是一个隐式的 uncurried 函数。Overture 都接受了所有内容。test4 是对隐式柯里化函数的尝试，但被 Overture 拒绝。

另外，有没有办法用隐式函数定义来指定它应该是全部的？

module moduleName
  exports all
  definitions
  functions

  test1 : nat * nat +> nat
  test1 (arg1,arg2) == arg1+arg2;

  test2 : nat -> nat +> nat
  test2 (arg1) (arg2) == arg1+arg2;

  test3 (arg1:nat,arg2:nat) res:nat
  post res = arg1+arg2;

  test4 (arg1:nat) (arg2:nat) res:nat
  post res = arg1+arg2;

end moduleName
4

1 回答 1

2

不，恐怕咖喱函数仅提供给显式函数定义。并且没有隐式定义的部分/全部指标。

（我只是问为什么我们会有这种差异。似乎与语言的历史有关：英语学校产生了隐含的功能但没有currying，而丹麦学校的显式功能有currying。它们真的应该被和谐 -你猜到的语法可能就是结果。）

于 2016-02-07T11:35:29.140 回答