1

更新1

  1. 我必须 cabal 安装 maude 才能使用 rewrite,如果不导入 maude,het 工具的 haskell 代码如何在其 haskell 代码中使用 rewrite 和 reduce?

  2. 如何以代数规范输入文件或默认系统和逻辑字符串作为参数来证明逻辑以将输出返回到控制台?有没有这方面的例子,并在 Scratch 中完成所有这些?

  3. 此外,想在 Scratch 中读取 Owl 文件并在 Scratch 中进行推理,有没有这样的例子?

https://github.com/spechub/Hets/blob/master/Scratch.hs

update2 成功运行第一个示例 RelationAndOrders.casl,但是,Scratch.hs 中流程的目标和输出是什么

martin@ubuntu:~/Downloads/Hets-master$ sudo cp Scratch /usr/lib/hets/hets-lib/Basic/Scratch
martin@ubuntu:~/Downloads/Hets-master$ cd /usr/lib/hets/hets-lib/Basic
martin@ubuntu:/usr/lib/hets/hets-lib/Basic$ ./Scratch RelationsAndOrders.casl 
### file name 'RelationsAndOrders.casl' does not match library name 'Basic/RelationsAndOrders'
Analyzing library Basic/RelationsAndOrders version 1.0
Downloading Basic/Numbers ...
Analyzing library Basic/Numbers version 1.0
Analyzing spec Basic/Numbers?Nat
Analyzing spec Basic/Numbers?Int
Analyzing spec Basic/Numbers?Rat
Analyzing spec Basic/Numbers?DecimalFraction
... loaded Basic/Numbers
Analyzing spec Basic/RelationsAndOrders?Relation
Analyzing spec Basic/RelationsAndOrders?ReflexiveRelation
Analyzing spec Basic/RelationsAndOrders?IrreflexiveRelation
Analyzing spec Basic/RelationsAndOrders?SymmetricRelation
Analyzing spec Basic/RelationsAndOrders?AsymmetricRelation
Analyzing spec Basic/RelationsAndOrders?AntisymmetricRelation
Analyzing spec Basic/RelationsAndOrders?TransitiveRelation
Analyzing spec Basic/RelationsAndOrders?SimilarityRelation
Analyzing spec Basic/RelationsAndOrders?PartialEquivalenceRelation
Analyzing spec Basic/RelationsAndOrders?EquivalenceRelation
Analyzing spec Basic/RelationsAndOrders?PreOrder
Analyzing spec Basic/RelationsAndOrders?StrictOrder
Analyzing spec Basic/RelationsAndOrders?PartialOrder
Analyzing spec Basic/RelationsAndOrders?TotalOrder
Analyzing spec Basic/RelationsAndOrders?StrictTotalOrder
Analyzing spec Basic/RelationsAndOrders?RightUniqueRelation
Analyzing spec Basic/RelationsAndOrders?LeftTotalRelation
Analyzing spec Basic/RelationsAndOrders?BooleanAlgebra
Analyzing spec Basic/RelationsAndOrders?ExtPartialOrder
Analyzing spec Basic/RelationsAndOrders?ExtTotalOrder
Analyzing spec Basic/RelationsAndOrders?ExtBooleanAlgebra
Analyzing spec Basic/RelationsAndOrders?RichPartialOrder
Analyzing spec Basic/RelationsAndOrders?RichTotalOrder
Analyzing spec Basic/RelationsAndOrders?RichBooleanAlgebra
Analyzing view Basic/RelationsAndOrders?TotalOrder_in_Nat
Analyzing view Basic/RelationsAndOrders?TotalOrder_in_Int
Analyzing view Basic/RelationsAndOrders?TotalOrder_in_Rat
Analyzing view Basic/RelationsAndOrders?PartialOrder_in_ExtBooleanAlgebra

更新3

运行 BasicSpec.casl 时

martin@ubuntu:~/Downloads/Hets-master/CASL/test$ ./Scratch BasicSpec.casl
Analyzing file BasicSpec.casl as library BasicSpec
Analyzing spec BasicSpec?BasicSpec

unexpected mixfix token: 252
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:710.31:
*** Error:
missing %number annotation
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:710.31:
*** Error:
unexpected mixfix token: 253
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:711.31:
*** Error:
missing %number annotation
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:711.31:
*** Error:
unexpected mixfix token: 254
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:712.31:
*** Error:
missing %number annotation
/home/martin/Downloads/Hets-master/CASL/test/BasicSpec.casl:712.31:
*** Error:
unexpected mixfix token: 255
Scratch: user error (Stopped due to errors)
4

0 回答 0