小编Die*_*ias的帖子

这是我的第一篇文章。因此，我希望这个问题令人兴奋。我有一个使用Swing + JPA来处理PostgreSQL数据库的Java程序。我使用EclipseLink JPA 2.0作为我的持久性提供程序。我的实体类是由Netbeans 7.2.1自动生成的

我面临的问题是：在更新期间，我更改了使用find（）检索到的对象的四个字段，然后使用merge（）更新了数据库中的对象。该表中识别并更新了四个更改中的三个，但是其中一个未更新。

我尝试了几种方法来解决此问题：我尝试更改与我的持久单元的同步策略相关的选项，更改代码中的行位置（其他字段已更新），我还尝试为Entity Class字段添加前缀带有注释@Basic（可选= false）。。我的任何尝试都有效。

这是我的实体类（Senha.java）的代码：

package model;

import java.io.Serializable;
import java.util.Date;
import javax.persistence.Basic;
import javax.persistence.Column;
import javax.persistence.Entity;
import javax.persistence.GeneratedValue;
import javax.persistence.GenerationType;
import javax.persistence.Id;
import javax.persistence.NamedQueries;
import javax.persistence.NamedQuery;
import javax.persistence.Table;
import javax.persistence.Temporal;
import javax.persistence.TemporalType;
import javax.xml.bind.annotation.XmlRootElement;

/**
 *
 * @author Diego Dias
 */
@Entity
@Table(name = "senha")
@XmlRootElement
@NamedQueries({
    @NamedQuery(name = "Senha.findAll", query = "SELECT s FROM Senha s"),
    @NamedQuery(name = "Senha.findById", query = "SELECT s FROM Senha s WHERE s.id = :id"), …

问题

我想知道在 Isabelle 中是否有一种自然的编码方式是这样的语法：

 type_synonym Var = string
 datatype Value = VInt int | ...
 datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ...

动机是根据非确定性选择定义一些规范命令，例如：

 Magic == NonDeterministicChoice {}
 Rely c r z = Defined using set compreehension and NonDeterministicChoice

Isabelle 抱怨“Cmd set”中类型“Cmd”的递归出现，即：

不支持通过类型表达式“Cmd set”中的类型构造函数“Set.set”递归出现类型“Cmd”。使用“bnf”命令将“Set.set”注册为有界自然函子以允许嵌套（共）递归通过它

在我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为“set”类型注册有界自然函子，因此我决定尝试一种推测性解决方案。

投机解决方案

相反，如果我使用归纳定义的数据类型，例如列表，伊莎贝尔不会抱怨，例如

datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...

列表在这里不是正确的抽象，但我试一试看看它是否有效。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题就变成了假设存在两个列表：一个包含Cmd 的所有元素，另一个包含Value 的所有元素。

我声明了两个未解释的常量：

consts Values :: "Value list"
consts Programs :: "Cmd …