iTask工作流管理系统语义与测试属性详解

### iTask工作流管理系统语义与测试属性详解 #### 1. 语义与测试属性基础 在语义和测试属性方面，我们使用逻辑组合符 `==>` ，它模拟逻辑中的蕴含关系 `⇒` 。例如属性 `pEnv3` 产生的结果是一个 `Property` 而非布尔值，这个运算符作为测试中使用值的额外约束。同时，在语义开发过程中发现的问题是可测试属性的宝贵来源。如果特定构造和值的语义存在问题，我们可以定义它应产生正确值的属性，若能将此类属性推广到所有值并引入全称量化变量则更佳。 #### 2. iTask系统概述 iTask系统支持工人通过基于Web的界面执行指定任务，典型的基本用户任务包括填写表单和按下按钮进行选择。这些基本任务基于iData系统实现，iTask系统根据输入确定要执行的新任务并更新浏览器界面。任意复杂的任务可通过组合基本任务创建，数据相关任务的真正强大之处在于单子绑定运算符，它包含一个根据前一个任务产生的值生成下一个任务的函数。 然而，iTask的实现需要同时处理许多其他事情，如文件和数据库的I/O、多用户Web界面的生成、任务的客户端/服务器评估以及异常处理等。为了克服实现过于复杂难以理解语义的问题，我们开发了iTask的高级操作语义，该语义是早期工作的扩展版本，用于解释iTask系统的行为并推理系统的期望行为，未来还将作为模型使用基于模型的测试工具G∀st来测试实际的iTask实现。 #### 3. iTask的形式化定义 在原始的iTask系统中，任务是严格且唯一的任务状态 `TSt` 的状态转换器，用类型注解 `*` 表示任务状态的唯一性，类型参数 `a` 表示任务完成时返回的结果类型。 ```haskell :: Task a :== *TSt →*(a,*TSt) // an iTask is a state transition of type TSt ``` 这里我们只考虑一个基本任务：编辑任务。 ```haskell editTask :: String a →Task a | iData a ``` `editTask` 函数接受一个字符串和类型为 `a` 的值作为参数，在类型 `a` 属于类型类 `iData` 的上下文限制下产生一个 `(Task a)` 。该函数创建一个GUI来修改给定类型的值，并添加一个带有给定名称的按钮来完成任务，用户可多次更改值，直到按下按钮任务才完成。对于所有基本数据类型都有预定义的编辑器，对于其他数据类型，可使用Clean的通用编程机制派生编辑器或为该类型定义定制编辑器。 同时，我们关注以下基本的iTask组合器来组合任务： | 组合器 | 定义 | 功能 | | ---- | ---- | ---- | | `return` | `:: a →Task a \| iData a` | 将值转换为立即产生该值的任务 | | `(>>=)` | `infixl 1 :: (Task a) (a→Task b) →Task b \| iData b` | 表示任务序列，先完成任务 `t` ，将结果传递给 `u` 以创建并执行新任务 | | `(-||-)` | `infixr 3 :: (Task a) (Task a) →Task a \| iData a` | 两个iTask可任意顺序执行和交错，任一子任务完成则组合任务完成，结果为首先完成的子任务的结果 | | `(-&&-)` | `infixr 4 :: (Task a) (Task b) →Task (a,b) \| iData a & iData b` | 两个iTask可任意顺序执行和交错，两个子任务都完成则组合任务完成，结果为包含两个子任务结果的元组 | 这些组合器是操作复杂任务状态 `TSt` 的高阶函数，为了便于推理iTask，我们将高阶函数和任务状态 `TSt` 替换为代数数据类型 `ITask` 。 ```haskell :: ITask = EditTask ID String BVal // an editor | .||. infixr 3 ITask ITask // OR-combinator | .&&. infixr 4 ITask ITask // AND-combinator | Bind ID ITask (Val→ITask) // sequencing-combinator | Return Val // return the value :: Val = Pair Val Val | BVal BVal :: BVal = String String | Int Int | VOID ``` 为了方便编写 `ITask` ，我们引入两个缩写： ```haskell (⇛) infixl 1 :: ITask (Val→ITask) →ITask (⇛) t f = Bind id1 t f ButtonTask i s t = EditTask i s VOID ⇛λ_ →t ``` #### 4. 任务标识 任务由基本子任务组成，子任务可由生成的Web界面中的事件更改，为了将这些事件与正确的子任务关联，我们使用自动系统来标识子任务。任务由整数列表标识，数据类型 `ID` 表示这些任务标识符。 ```haskell :: ID = ID [Int] next :: ID →ID next (ID [a:x]) = ID [a+1:x] splitID :: ID →[ID] splitID (ID i) = [ID [0 ,j:i] \\ j ←[0.. ]] nmbr :: ID ITask →ITask nmbr i (EditTask _ s v) = EditTask i s v ```