代码之家 › 专栏 › 技术社区 › mnuzzo

在合金中按日期获取项目

alloy formal-methods

0

mnuzzo · 技术社区 · 15 年前

我被这个正式的家庭作业问题困住了,我不确定我没有做对什么。

我有两个签名,Item和ToDo,其定义如下:

sig Item {
    due : Date lone -> Step,
    category : Category lone -> Step
}

one sig ToDo {
    list : (seq Item) -> Step,
    current : Item lone -> Step,
    completed : Item -> Step
}

我必须定义一个函数,将具有给定日期和类别的项插入到ToDo列表集中。诀窍在于,列表集应该按项目的截止日期排序。步骤和日期都有订单。

我的问题是:如何获取ToDo中的项目集。列出具体日期?我有一个函数:

fun tasksWithDate[d : Date, st : Step, t : set Item]: set Item

我尝试使用以下代码(及其变体)来获取项目集:

t.due.st.d

这不管用,我明白为什么,因为t.due。st会留下一组日期。然而,从那一点出发的其他尝试并没有让我达到目的。在到达t之前,我尝试使用括号来计算“due.st”和“d”之间的连接,但这不起作用,我尝试使用方括号来更改顺序,但这不起作用。我知道我做错了什么,但我不知道是什么。

1 回复 | 直到 15 年前

1

mnuzzo 15 年前

我提出的解决方案如下:

let r = t -> t.due.st {
    r.d
}

它所做的是创建一组t与到期日t的关系。然后,它执行一个与所需日期的连接,返回该日期的所有t。