软件规范开发辅助方法以及软件规范开发辅助装置

摘要

一种软件规范开发辅助方法以及软件规范开发辅助装置。规范检查部，对于从命题规则保存部取得的任意的检查对象的命题形式的规范和其任意的比较对象的命题形式的规范，判定2个命题形式的规范是否矛盾或重复，如果矛盾或重复，则将所述作为检查对象的命题形式的规范分解为与比较对象的命题形式的规范矛盾或重复的命题形式的规范、以及与比较对象的命题形式的规范不矛盾或不重复的命题形式的规范，登录在检查结果保存部中，决定表生成部从检查结果保存部取得所述命题形式的规范的任意一方或双方，关于各个所述命题形式的规范取出该命题形式的规范的条件部和结果部来生成决定表的行，将显示范围表示在与该命题形式的规范对应的列的相应行的栏中。

说明书

技术领域

本发明涉及一种辅助软件开发的技术。

背景技术

有时候会用软件执行前的条件和其执行后的结果的对应关系来定义软件 的规范。已知该条件和结果的对应关系可以用被称为决定表（decision table） 的表形式来表现，被频繁地用于软件开发工程。决定表中有几种不同的记述形 式，但即使是记述形式不同的决定表，表示条件和结果的对应关系的语义也是 一样的。而且，决定表有时候也被称为条件矩阵或检查列表等其他名称。

通过使用该决定表来表示规范，可以准确无误地记述条件和结果的对应关 系，同时还有容易发现条件的模式遗漏的效果。另一方面，基于决定表的规范 记述有以下缺点。即，存在随着条件要素的增加，模式增加且决定表扩大，从 而可读性下降的问题。

作为解决该问题的现有技术，专利文献1公开了一种通过分割决定表进行 表述来防止可读性下降的方法。

若使用专利文献1公开的现有技术，可以用可读性高的形式来显示决定 表。但是由于决定表的记述量不变，因此会产生决定表的输入量增加、生成工 时增加的问题和为了保存决定表所需的存储容量增大的问题。作为解决该问题 的现有技术，专利文献2公开了一种方法，即通过从命题形式的记述来生成决 定表，从而削减决定表的生成工时。另外，公开以下方法，即通过从决定表提 取命题形式的记述后进行保存/显示，从而削减为了保存/显示决定表所需的存 储容量。

但是，当规范有矛盾或遗漏时，与决定表形式的规范显示相比，基于命题 形式的记述的规范显示具有难以视觉确认矛盾或遗漏的缺点。也就是说，要想 通过决定表的显示来视觉确认矛盾或遗漏时，专利文献2所表示的方法没有 效。因此，为了提高规范的矛盾或遗漏的视觉辨认性而以决定表形式进行规范 显示时，由于不能应用专利文献2所表示的现有技术，所以不能解决随着决定 表的扩大化而决定表的显示所需的存储容量增大的问题。另外，专利文献2 所示的现有技术，在基于命题形式的记述的规范显示之前在内部生成决定表。 因此现有技术也有随着决定表的扩大化，决定表的生成所需的存储容量和处理 时间增大的问题。

[专利文献1]日本特开2005-44303号公报

[专利文献2]日本特愿2011-052340号公报

发明内容

鉴于上述情况而提出本发明，其目的为提供一种技术，一边维持用于提高 规范的矛盾或遗漏的视觉辨认性的决定表形式的显示，一边削减决定表的生成 以及显示所需的存储容量。

以下为本发明的具有代表性的一例。即，本发明的软件规范开发辅助装置 具备：命题规范接受部，其经由输入部接受由具有多个条件的条件部以及具有 多个结果的结果部组成的多个命题形式的规范；第1保存部，其保存多个命题 形式的规范；规范检查部，其根据所述第1保存部的命题规范判定所述多个命 题形式的规范的各个规范是否相互矛盾或者重复，将其结果保存在第2保存部 中；决定表生成部，其根据所述检查的结果生成以表形式表示的决定表，所述 表形式由各行表示所述多个条件之一或者所述多个结果之一，各列表示所述多 个命题形式的规范的各个规范。所述规范检查部，对于从所述第1保存部取得 的任意的作为检查对象的命题形式的规范和其任意的作为比较对象的命题形 式的规范，判定所述2个命题形式的规范是否矛盾或者重复，如果矛盾或者重 复，则将所述作为检查对象的命题形式的规范分解为与作为比较对象的命题形 式的规范矛盾或者重复的命题形式的规范、以及与作为比较对象的命题形式的 规范不矛盾且不重复的命题形式的规范，登录在所述第2保存部中，所述决定 表生成部从所述第2保存部取得所述命题形式的规范的任意一方或者双方，关 于各个所述命题形式的规范，取出该命题形式的规范的条件部和结果部来生成 所述决定表的行，将显示范围表示在与该命题形式的规范对应的列的相应行的 栏中。

根据本发明，可以在决定表上视觉确认规范的矛盾、重复，可以削减该决 定表的生成以及显示所需的存储容量。

附图说明

图1是表示软件规范开发辅助装置201的结构例的框图。

图2是表示软件规范开发辅助装置201的硬件结构例的框图。

图3是命题规则保存部102所保存的命题规则的例子。

图4是构成命题规则的条件项目和结果项目的例子。

图5是制约保存部104所保存的制约的例子。

图6是矛盾检查部105在检查结果保存部109中登录的矛盾检查结果的例 子。

图7是表示矛盾检查的步骤例的流程图。

图8是重复检查部106在检查结果保存部109中登录的重复检查结果的例 子。

图9是表示重复检查的步骤例的流程图。

图10是根据重复检查的结果生成的文氏逻辑运算图的例子。

图11是未定义检查部107在检查结果保存部109中登录的未定义检查结 果的例子。

图12是表示未定义检查的步骤例的流程图。

图13是制约检查部108在检查结果保存部109中登录的检查结果的例子。

图14是表示制约检查的步骤例的流程图。

图15是策略保存部111所保存的显示策略的例子。

图16是显示对象规则保存部115所保存的显示对象规则的例子。

图17是表示显示对象规则决定的步骤例的流程图。

图18是决定表部分显示/修正部116根据显示对象规则保存部115所保存 的显示对象规则进行显示的部分决定表的例子。

图19是决定表部分显示/修正部116通过接受修正输入而被修正的部分决 定表的例子。

图20是修正完毕规则保存部118所保存的修正完毕规则的例子。

符号说明

101：命题规则编辑部；102：命题规则保存部；103：制约编辑部；104： 制约保存部；105：矛盾检查部；106：重复检查部；107：未定义检查部；108： 制约检查部；109：检查结果保存部；110：可选择策略设定部；111：策略保 存部；112：策略选择部；113：策略编辑部；114：显示对象规则决定部；115： 显示对象规则保存部；116：决定表部分显示/修正部；117：修正完毕规则生 成部；118：修正完毕规则保存部；119：修正完毕规则置换部。

具体实施方式

以下参照附图详细说明本发明的一个实施方式。

本实施方式适用于辅助软件使用的开发的装置。

本实施方式中，接受通过命题形式的记述进行的规范（称为命题规则）的 输入，检查命题规则间的矛盾、遗漏、重复以及差分。还接受对于命题规则的 制约，检查命题规则的制约违反。并且根据检查结果来生成表示与检查结果有 关的规范的命题形式的记述（称为显示对象规则）。进一步，根据生成的显示 对象规则生成并显示决定表。

因此，根据本实施方式，可以在决定表上确认规范的矛盾、遗漏、重复、 差分以及制约违反的检查结果，可以削减该决定表的生成以及显示所需的存储 容量。

另外，在本实施方式中，在根据显示对象规则所生成的决定表上接受规范 的修正。还有，根据修正完毕的决定表生成反映了修正的显示对象规则（称为 修正完毕规则），和原来的显示对象规则进行替换。

因此，根据本实施方式可以不对命题记述而是对规范视觉辨认性高的决定 表进行规范的修正，从而能够削减修正错误。

本实施方式，根据所述检查结果，保存用于生成成为决定表显示对象的显 示对象规则的显示策略。并且在决定表显示之前接受所述显示策略的有效/无 效的设定，根据被选择的显示策略来生成成为决定表显示对象的显示对象规 则。

因此，根据本实施方式，可以考虑规范的规模和所述检查结果来调整决定 表显示对象的规范量，因此可以防止生成以及显示的决定表的扩大化。

本实施例中的所述命题规则、制约、显示对象规则以及修正完毕规则等的 命题形式的记述，设想自然语言形式以及逻辑式形式这两种。命题规则、显示 对象规则以及修正完毕规则由条件部和结果部构成。条件部由条件项目值的逻 辑积构成。同样，结果部由结果项目值的逻辑积构成。制约由前项和后项构成。 制约的前项和命题规则的条件部一样，由条件项目值的逻辑积构成。后项也一 样由条件项目值的逻辑积构成。

例如，假定存在条件项目A、B和结果项目C，分别取a1和a2、b1和b2、 c1和c2的值。这时候可以记述“当A是a1且B不是b1时，C是c1”的命题 规则。该命题规则也可以通过逻辑式形式记述为条件部是“A=a1∧B≠b1”，结果部是“C=c1”。本实施例中使用自然语言形式 以及逻辑式形式两种方式来表示例子。

图1是表示本实施方式中的软件规范开发辅助装置201的结构例的框图。

软件规范开发辅助装置201包括命题规则编辑部101、命题规则保存部 102、制约编辑部103、制约保存部104、矛盾检查部105、重复检查部106、 未定义检查部107、制约检查部108、检查结果保存部109、可选择策略设定 部110、策略保存部111、策略选择部112、策略编辑部113、显示对象规则决 定部114、显示对象规则保存部115、决定表部分显示/修正部116、修正完毕 规则生成部117、修正完毕规则保存部118以及修正完毕规则置换部119。

命题规则编辑部101接受命题规则的输入以及编辑，将接受的命题规则登 录在命题规则保存部102中。

制约编辑部103接受对命题规则的制约的输入以及编辑，将接受的制约登 录在制约保存部104中。

矛盾检查部105从命题规则保存部102取得命题规则。从取得的命题规则 中决定检查对象规则和其比较对象规则，检查检查对象规则和比较对象规则的 矛盾。检查结果登录在检查结果保存部109中。检查对象规则和比较对象规则 可以根据来自外部的用户的输入来决定。

重复检查部105从命题规则保存部102取得命题规则。从取得的命题规则 中决定检查对象规则和其比较对象规则，检查基于检查对象规则和比较对象规 则的规范的重复定义。在命题规则中设定了优先度时，检查基于检查对象规则 和比较对象规则的规范的覆盖。另外，当检查对象规则和比较对象规则与同一 规则的变更前和变更后对应时，检查其差分规范。这些检查结果登录在检查结 果保存部109中。检查对象规则和比较对象规则可以根据来自外部的输入来决 定。

另外，矛盾检查部105和重复检查部106可以根据检查结果来显示表示检 查对象规则和比较对象规则的关系的文氏逻辑运算图。

未定义检查部107从命题规则保存部102取得命题规则，检查没有被命题 规则定义的未定义规范。检查结果登录在检查结果保存部109中。正如对于某 个结果项目C“C不是c1”那样，即使只定义“不是～”规范的时候，结果项 目C也可以是未定义。

制约检查部108从命题规则保存部102取得命题规则，同时从制约保存部 104取得制约。检查所取得的命题规则是否满足同样取得的制约。检查结果登 录在检查结果保存部109中。

检查结果保存部109保存检查结果。检查结果至少包括通过各自的检查而 得到的命题形式的规范。

可选择策略设定部110从检查结果保存部109取得检查结果。并且根据取 得的检查结果，从策略保存部111所保存的显示策略中挑选满足适用条件的可 适用的策略。

策略选择部112接受显示策略的有效或者无效的输入，将策略保存部111 所保存的策略切换为有效或者/无效。

策略编辑部113接受显示策略编辑的输入，变更策略保存部111所保存的 策略。

显示对象规则决定部114从策略保存部111取得可适用的显示策略。还从 检查结果保存部109取得包括命题形式的规范的检查结果。根据取得的显示策 略和检查结果来决定显示对象规则。得到的显示对象规则登录在显示对象规则 保存部115中。

决定表部分显示/修正部116从显示对象规则保存部115取得显示对象规 则，以决定表形式来显示所述显示对象规则的表示规范。另外，接受已显示的 决定表的修正输入，变更以决定表形式所显示的规范。

修正完毕规则生成部117取得决定表部分显示/修正部116所显示/修正的 决定表，将决定表的表示规范变换为命题形式的规范。通过变换而得到的命题 形式的规范作为修正完毕规则登录在修正完毕规则保存部118中。

修正完毕规则置换部119从修正完毕规则保存部118取得修正完毕规则， 同时从检查结果保存部109取得包括修正前的显示对象规则的检查对象规则。 接着，通过将修正前的显示对象规则置换为修正完毕规则，得到表示修正完毕 的检查对象规则的命题形式的规范。最后，将得到的命题形式的规范置换为命 题规则保存部102所保存的检查对象规则。

图2是表示软件规范开发辅助装置201的硬件结构例的图。

软件规范开发辅助装置201具备CPU202、存储器203、外部存储装置204、 显示装置205、输入装置206以及外部介质输入输出装置207。

CPU202通过执行存储器203所存储的程序来执行各种处理。存储器203 作为CPU202的工作区域发挥功能，存储程序以及程序的执行所需的数据。具 体地说，存储构成命题规则编辑部101、制约编辑部103、矛盾检查部105、 重复检查部106、未定义检查部107、制约检查部108、可选择策略设定部110、 策略选择部112、策略编辑部113、显示对象规则决定部114、决定表部分显 示/修正部116、修正完毕规则生成部117以及修正完毕规则置换部119的程序， 同时存储命题规则保存部102、制约保存部104、检查结果保存部109、策略 保存部111、显示对象规则保存部115以及修正完毕规则保存部118所保存的 数据。

外部存储装置204存储各种数据。外部存储装置204例如是硬盘装置等。 具体地说，存储命题规则保存部102、制约保存部104、检查结果保存部109、 策略保存部111、显示对象规则保存部115以及修正完毕规则保存部118。

或者，可以在外部存储装置204中存储构成命题规则编辑部101、制约编 辑部103、矛盾检查部105、重复检查部106、未定义检查部107、制约检查部 108、可选择策略设定部110、策略选择部112、策略编辑部113、显示对象规 则决定部114、决定表部分显示/修正部116、修正完毕规则生成部117以及修 正完毕规则置换部119的程序的至少一部分，当执行各种处理时CPU202将其 读出到存储器203并执行程序。另外，各个程序可以被预先存储到存储器203 或者外部存储装置204中，也可以根据需要，经由可使用的介质从其他装置导 入到存储器203或者外部装置204中。所谓介质，是指例如可在外部介质输入 输出装置207上装卸的存储介质，或者网络、在网络上传播的载波和数字信号 等通信介质。

显示装置205显示程序的处理结果等。显示装置205例如是显示器等。输 入装置206从使用者接受处理的执行指示以及处理所需的信息的输入等。输入 装置206例如是键盘以及鼠标等。

外部介质输入输出装置207对存储在外部介质和外部存储装置204中的数 据等进行输入输出。外部介质是可在外部介质输入输出装置207上装卸的可移 动性存储介质，外部介质输入输出装置207是可在外部介质中进行读写的驱动 装置等。

图3是命题规则保存部102所保存的命题规则的例子。另外，图4是构成 命题规则的条件项目和结果项目的例子。

条件项目401由条件项目名称402和该项目的值即条件值403构成。同样， 结果项目404由结果项目名称405和该项目的值即结果值构成。例如，命题规 则301表示“当保险加入有无的名称的条件项目的值是已加入时，补助金的名 称的结果项目值是有交付”的规范。命题规则301的条件部为““保险加入有 无”是“已加入””，结果部为““补助金”是“有交付””。

图5是制约保存部104所保存的制约的例子。

例如，制约501表示“当保险加入有无的名称的条件项目的值是未加入时， 保险缴纳额的名称的条件项目的值是0日元”的制约。制约501的前项为““保 险加入有无”是“未加入””，后项为““保险缴纳额”是“0日元””。

图6是矛盾检查部105在检查结果保存部109中登录的矛盾检查结果的例 子。

矛盾检查的检查结果601由检查对象规则602、比较对象规则603、检查 结果604、矛盾的规范605以及不矛盾的规范606构成。

检查对象规则602以及比较对象规则603表示命题规则中分别成为矛盾检 查的对象的命题规则和成为其比较对象的命题规则。检查结果604表示检查对 象规则602和比较对象规则603的矛盾检查结果。矛盾的规范605表示在检查 对象规则602所表示的规则中与比较对象规则603所表示的规范矛盾的规范。 相反，不矛盾的规范606表示在检查对象规则602所表示的规范中与比较对象 规则603所表示的规范不矛盾的规范。

例如，假定作为检查对象规则602而给出命题规则301，作为其比较对象 规则603而给出命题规则302。这时，矛盾检查部105登录“有矛盾”作为检 查结果604。同时，作为矛盾的规范605，登录以下规范，即“当“保险加入 有无”是“已加入”，且“保险缴纳额”是“2万日元以上”时，“补助金”是 “有交付””。进一步，作为不矛盾的规范606，登录以下规范，即“当“保险 加入有无”是“已加入”，且“保险缴纳额”不是“2万日元以上”时，“补助 金”是“有交付””。

图7是表示矛盾检查的步骤例的流程图。

以下所示的处理是通过软件规范开发辅助装置201所具备的CPU202在存 储器203中执行的程序来实现的。并且，该程序由进行以下说明的各种动作的 代码构成。

CPU202通过执行矛盾检查部105，从命题规则保存部102取得任意的2 个命题规则，分别作为检查对象规则以及比较对象规则。取得的检查对象规则 和比较对象规则分别登录在检查结果保存部109的检查对象规则602和比较对 象规则603中（步骤701）。

矛盾检查部105参照表示取得的检查对象规则的条件的条件部和表示比 较对象规则的条件的条件部，判定双方的条件部是否并存。当条件部并存时， 接着参照表示检查对象规则的结果的结果部和表示比较对象规则的结果的结 果部，判定双方的结果部是否并存。当条件部并存并且结果部不并存时，在检 查结果保存部109的检查结果604中登录“有矛盾”，执行步骤703。当条件 部不并存，或者条件部并存但结果部也并存时，在检查结果保存部109的检查 结果604中登录“不矛盾”，在不矛盾的规范606中登录检查对象规则并结束 处理。所述并存性的检查中可以使用SAT解算器。例如命题规则301和命题 规则302的条件部并存且结果部不并存，因此在检查结果604中登录“有矛盾”， 执行步骤703。（步骤702）。

矛盾检查部105检查是否有出现在比较对象规则中而没有出现在检查对 象规则中的条件项目。当有符合所述条件的条件项目时执行步骤704。当没有 符合所述条件的条件项目时执行步骤706。例如将命题规则301作为检查对象 规则，将命题规则302作为比较对象规则时，“保险缴纳额”的条件项目符合 所述条件，因此执行步骤704（步骤703）。

矛盾检查部105将在步骤703检测出的、出现在比较对象规则中而没有出 现在检查对象规则中的条件项目以与比较对象规则中出现的值相同的值在检 查对象规则的条件部进行逻辑积结合。例如上述例子的情况下，将““保险缴 纳额”是“2万日元以上””的条件在命题规则301的条件部进行逻辑积结合， 得到当“保险加入有无”是“已完毕”且“保险缴纳额”是“2万日元以上” 时，“补助金”是“有交付”的记述。（步骤704）。

矛盾检查部105将在步骤704生成的记述作为矛盾的规范605登录在检查 结果保存部109中（步骤705）。

矛盾检查部105将检查对象规则作为矛盾的规范605登录在检查结果保存 部109中，结束处理（步骤706）。

矛盾检查部105将在步骤703检测出的、出现在比较对象规则中而没有出 现在检查对象规则中的条件项目以比较对象规则中出现的值的否定值在检查 对象规则的条件部进行逻辑积结合。例如在上述例子的情况下，将““保险缴 纳额”不是“2万日元以上””的条件在命题规则301的条件部进行逻辑积结 合，得到当“保险加入有无”是“已加入”且“保险缴纳额”不是“2万日元 以上”时，“补助金”是“有交付”的记述。（步骤707）。

矛盾检查部105将在步骤707生成的记述作为不矛盾的规范606登录在检 查结果保存部109中（步骤708）。

图8是重复检查部106在检查结果保存部109中登录的重复检查结果的例 子。

重复检查的检查结果801由检查对象规则802、比较对象规则803、检查 结果804、重复的规范805以及不重复的规范806构成。

检查对象规则802以及比较对象规则803表示命题规则中分别成为重复检 查对象的命题规则和成为其比较对象的命题规则。检查结果804表示检查对象 规则802和比较对象规则803的重复检查结果。重复的规范805表示在检查对 象规则802所表示的规范中、与比较对象规则803所表示的规范重复的规范。 相反，不重复的规范806表示在检查对象规则802所表示的规范中、与比较对 象规则803所表示的规范不重复的规范。

例如，假定作为检查对象规则802而给出命题规则301，作为其比较对象 规则803而给出命题规则303。这时，重复检查部106作为检查结果804而登 录“有重复”。同时，作为重复的规范805，登录以下规范，即“当“保险加 入有无”是“已加入”且“保险缴纳额”是“2万日元以上”时，“补助金” 是“有交付””，作为不重复的规范806，登录以下规范，即“当“保险加入有 无”是“已加入”且“保险缴纳额”不是“2万日元以上”时，“补助金”是 “有交付””。

另外，所述的重复检查部106不仅检查命题规则间的规范的重复，也可以 进行覆盖检查和差分检查。覆盖检查时，将在检查对象规则802所表示的规范 中对比较对象规则803所表示的规范进行覆盖的规范、或者通过比较对象规则 803所表示的规范而被覆盖的规范登录在重复的规范805中。差分检查时，将 检查对象规则802所表示的规范中与比较对象规则803所表示的规范的差分的 规范登录在重复的规范805中。

图9是表示重复检查的步骤例的流程图。

以下所示的处理是通过决定表生成辅助/验证装置201所具备的CPU202 在存储器203中执行的程序来实现的。并且，该程序由进行以下所说明的各种 动作的代码构成。

CPU202通过执行重复检查部106从命题规则保存部102取得任意2个命 题规则，分别作为检查对象规则以及比较对象规则。取得的检查对象规则和比 较对象规则分别登录在检查结果保存部109的检查对象规则802和比较对象规 则803中（步骤901）。

重复检查部106参照表示取得的检查对象规则的条件的条件部和表示比 较对象规则的条件的条件部，判定双方的条件部是否并存。当条件部并存时， 在检查结果保存部109的检查结果804中登录“有重复”，执行步骤903。当 条件部不并存时，在检查结果保存部109的检查结果804中登录“没有重复”， 在不重复的规范806中登录检查对象规则并结束处理。所述并存性的检查中可 以使用SAT解算器。例如命题规则301和命题规则302的条件部并存，因此 在检查结果804中登录“有重复”，执行步骤903。（步骤902）。

重复检查部106检查是否有出现在比较对象规则中而没有出现在检查对 象规则中的条件项目。当有符合所述条件的条件项目时执行步骤904。当没有 符合所述条件的条件项目时执行步骤906。例如将命题规则301作为检查对象 规则，将命题规则302作为比较对象规则时，“保险缴纳额”的条件项目符合 所述条件，因此执行步骤904（步骤903）。

重复检查部106将在步骤903检测出的、出现在比较对象规则中而没有出 现在检查对象规则中的条件项目以与比较对象规则中出现的值相同的值在检 查对象规则的条件部进行逻辑积结合。例如在上述例子的情况下，将““保险 缴纳额”是“2万日元以上””的条件在命题规则301的条件部进行逻辑积结 合，得到当“保险加入有无”是“已加入”且“保险缴纳额”是“2万日元以 上”时，“补助金”是“有交付”的记述。（步骤904）。

重复检查部106将在步骤904生成的记述作为重复的规范805登录在检查 结果保存部109中（步骤905）。

重复检查部106将检查对象规则作为重复的规范805登录在检查结果保存 部109中，结束处理（步骤906）。

重复检查部106将在步骤903检测出的、出现在比较对象规则中而没有出 现在检查对象规则中的条件项目以比较对象规则中出现的值的否定值在检查 对象规则的条件部进行逻辑积结合。例如在上述例子的情况下，将““保险缴 纳额”不是“2万日元以上””的条件在命题规则301的条件部进行逻辑积结 合，得到当“保险加入有无”是“已加入”且“保险缴纳额”不是“2万日元 以上”时，“补助金”是“有交付”的记述。（步骤907）。

重复检查部106将在步骤907生成的记述作为不重复的规范806登录在结 果保存部109中（步骤908）。

图10是根据重复检查的结果生成的文氏逻辑运算图的例子。

范围1001表示检查对象规则即命题规则301所表示的规范的范围。范围 1002表示比较对象规则即命题规则302所表示的规范的范围。范围1003表示 检查对象规则所表示的规范中、与比较对象规则所表示的规范不重复的规范的 范围。范围1004表示检查对象规则所表示的规范中、与比较对象规则所表示 的规范重复的规范的范围。

图11是未定义检查部107在检查结果保存部109中登录的未定义检查结 果的例子。

未定义检查的检查结果1101由未定义条件1102构成。未定义条件1102 表示通过命题规则保存部102所保存的命题规则，结果未被定义的条件。

例如，当命题规则保存部109保存命题规则301、302以及303时，对于 ““保险加入有无”是“已加入”时”、““保险加入有无”是“已加入”时” 以及““保险缴纳额”是“2万日元以上”时”的条件，结果是定义完毕。另 一方面，对于““保险加入有无”是“未加入”且“保险缴纳额”是“1日元 以上不到2万日元”时”和““保险加入有无”是“未加入”且“保险缴纳额” 是“0日元”时”的条件，结果是未定义。因此，在未定义条件1102登录这2 个条件。

图12是表示未定义检查的步骤例的流程图。

以下所示的处理是通过决定表生成辅助/验证装置201所具备的CPU202 在存储器203中执行的程序来实现的。并且该程序由进行以下说明的各种动作 的代码构成。

CPU202通过执行未定义检查部107，从命题规则保存部102取得所有的 命题规则（步骤1201）。

未定义检查部107对于取得的各个命题规则，生成表示它们的条件部的否 定的记述。但是，在生成条件部的否定时，关于任意条件项目的X的任意值 x1，不可使用““X”不是“x1””的记述。在上述情况下，使用条件项目X的 x1以外的值x_i、x_i+1…x_j，使用““X”是“x_i”、或者“X”是“x_i+1”、…、 或者“X”是“x_j””这样的记述。同样，在逻辑式形式的记述中不可使用不 等号“≠”。

这里，假定被赋予条件项目A、B和结果项目C，分别取a1和a2、b1和 b2、c1和c2的值。这时，对于这样的命题规则， 作为其条件部的否定，生成“A=a2∨B=b1”的记述（步骤1202）。

未定义检查部107将表示在步骤1202生成的条件部的否定的记述进行逻 辑积结合（步骤1203）。

未定义检查部107将在步骤1203生成的记述变形为积和标准形（步骤 1204）。

未定义检查部107将在步骤1204生成的积和标准形的记述按每个合成子 句进行分离，将每个合成子句作为未定义条件1102登录在检查结果保存部109 中（步骤1205）。

图13是制约检查部108在检查结果保存部109中登录的制约检查结果的 例子。

制约检查的检查结果1301由检查对象规则1302、制约1303、检查结果 1304、制约对象的规范1305以及制约对象外的规范1306构成。

检查对象规则1302以及制约1303表示成为制约检查对象的命题规则和其 制约。检查结果1304表示对于检查对象规则1302的制约1303的制约检查的 结果。制约对象的规范1305表示在检查对象规则1302所表示的规范中、制约 1303的制约对象的规范。相反，制约对象外的规范1306表示检查对象规则1302 所表示的规范中、制约1303的制约对象外的规范。

例如，假定作为检查对象规则1302而给出命题规则302，作为制约1303 而给出制约501。这时，制约检查部108登录“有对象”作为检查结果1304。 同时，作为制约对象的规范1305，登录以下规范，即“当“保险加入有无” 是“未加入”且“保险缴纳额”是“2万日元以上”时，“补助金”是“没有 交付””，作为制约对象外的规范1306，登录以下规范，即“当“保险加入有 无”不是“未加入”且“保险缴纳额”是“2万日元以上”时，“补助金”是 “没有交付””。

图14是表示制约检查的步骤例的流程图。

以下所示的处理是通过决定表生成辅助/验证装置201所具备的CPU202 在存储器203中执行的程序来实现的。并且该程序由进行以下说明的各种动作 的代码构成。

CPU202通过执行制约检查部108从命题规则保存部102取得任意1个命 题规则作为检查对象规则。同时从制约保存部104取得任意1个制约。取得的 检查对象规则和制约分别登录在检查保存部109的检查对象规则1302和制约 1303中（步骤1401）。

制约检查部108参照取得的检查对象规则和制约，判定检查对象规则的条 件部和制约的前项是否并存。当并存时执行步骤1403。当不并存时，在检查 结果保存部109的检查结果1304中登录“没有对象”，在制约对象外的规范 1306中登录检查对象规则并结束处理。所述并存性的检查中可以使用SAT解 算器（步骤1402）。

制约检查部108判定检查对象规则的条件部和制约的后项是否并存。当并 存时执行步骤1404。当不并存时执行步骤1409。所述并存性的检查中可以使 用SAT解算器。例如命题规则302和制约501的情况下，条件部和前项并存， 但是条件部和后项不并存，因此执行步骤1409。另外考虑““保险加入有无” 是“未加入”时“补助金”是“有交付””的命题规则304的话，命题规则304 和制约501的情况下，条件部和前项并存，条件部和后项也并存，因此执行步 骤1404（步骤1403）。

制约检查部108检查是否有出现在制约的后项中而没有出现在检查对象 规则的条件部中的条件项目。当有符合所述条件的条件项目时，在检查结果保 存部109的检查结果1304中登录“有对象”，执行步骤1405。当没有符合所 述条件的条件项目时，在检查结果1304中登录“没有对象”，在制约对象外的 规范1306中登录检查对象规则并结束处理。例如命题规则304和制约501的 情况下，“保险缴纳额”的条件项目符合所述条件，因此在检查结果1304中登 录“有对象”，执行步骤1405（步骤1404）。

制约检查部108将在步骤1404检测出的、出现在制约的后项中而没有出 现在检查对象规则的条件部中的条件项目以制约的后项中出现的值的否定值 在检查对象规则的条件部进行逻辑积结合。例如命题规则304和制约501的情 况下，将““保险缴纳额”不是“0日元””的条件在命题规则301的条件部进 行逻辑积结合，得到“当“保险加入有无”是“未加入”且“保险缴纳额”不 是“0日元”时，“补助金”是“有交付””的记述（步骤1405）。

制约检查部108将在步骤1405中生成的记述作为制约对象的规范1305 登录在结果保存部109中（步骤1406）。

制约检查部108将在步骤1404检测出的、出现在制约的后项中而没有出 现在检查对象规则的条件部中的条件项目以与制约的后项中出现的值相同的 值在检查对象规则的条件部进行逻辑积结合。例如命题规则304和制约501 的情况下，将““保险缴纳额”是“0日元””的条件在命题规则301的条件部 进行逻辑积结合，得到“当“保险加入有无”是“未加入”且“保险缴纳额” 是“0日元”时，“补助金”是“有交付””的记述（步骤1407）。

制约检查部108将在步骤1407中生成的记述作为制约对象外的规范1306 登录在结果保存部109中（步骤1408）。

制约检查部108检查是否有出现在制约的前项中而没有出现在检查对象 规则的条件部中的条件项目。当有符合所述条件的条件项目时，在检查结果保 存部109的检查结果1304中登录“有对象”，执行步骤1411。当没有符合所 述条件的条件项目时，在检查结果1304中登录“有对象”，执行步骤1410。 例如命题规则302和制约501的情况下，“保险加入有无”的条件项目符合所 述条件，因此在检查结果1304中登录“有对象”，执行步骤1411（步骤1409）。

制约检查部108将检查对象规则作为制约对象的规范1305登录在检查结 果保存部109中，结束处理（步骤1410）。

制约检查部108将在步骤1409检测出的、出现在制约的前项中而没有出 现在检查对象规则的条件部中的条件项目以与制约的前项中出现的值相同的 值在检查对象规则的条件部进行逻辑积结合。例如命题规则302和制约501 的情况下，将““保险加入有无”是“未加入””的条件在命题规则302的条件 部进行逻辑积结合，得到“当“保险加入有无”是“未加入”且“保险缴纳额” 是“2万日元以上”时，“补助金”是“没有交付””的记述。（步骤1411）。

制约检查部108将在步骤1411中生成的记述作为制约对象的规范1305登 录在结果保存部109中（步骤1412）。

制约检查部108将在步骤1404检测出的、出现在制约的前项中而没有出 现在检查对象规则的条件部中的条件项目以制约的前项中出现的值的否定值 在检查对象规则的条件部进行逻辑积结合。例如命题规则302和制约501的情 况下，将““保险加入有无”不是“未加入””的条件在命题规则304的条件部 进行逻辑积结合，得到“当“保险加入有无”不是“未加入”且“保险缴纳额” 是“2万日元以上”时，“补助金”是“没有交付””的记述。（步骤1413）。

制约检查部108将在步骤1413中生成的记述作为制约对象外的规范1306 登录在结果保存部109中（步骤1414）。

图15是策略保存部111所保存的显示策略的例子。

显示策略一览1501由策略记述1502、策略适用条件1503、显示方法1504 以及有效/无效属性1505构成。

策略记述1502是与从检查结果中提取显示对象规则的方法有关的策略的 记述。显示对象规则决定部114根据解释策略记述1502的结果来决定显示对 象规则。策略适用条件1503表示用于应用策略的条件。未满足适用条件的策 略不能作为显示对象规则决定部114决定显示对象规则的策略而被应用。显示 方法1504表示根据该策略而决定的显示对象规则的、决定表上的显示方法。 有效/无效属性1505表示该策略当前有效还是无效。即使满足策略适用条件 1503，无效的策略也不被应用。

例如No.1的策略表示当检查结果保存部109保存有矛盾检查的检查结果 601时，将矛盾的规范605的规范决定为显示对象规则，在决定表上进行强调 显示。

No.5的策略表示当检查结果保存部109保存有矛盾检查的检查结果601 时，将不矛盾的规范606的规范决定为显示对象规则，在决定表上（不强调） 进行普通显示。

No.6的策略表示当检查结果保存部109保存有矛盾检查的检查结果601 时，取得与No.1的策略所表示的矛盾的规范605有8成以上的条件值一致的 命题规则，在决定表上进行普通显示。应用这样的策略时，显示对象规则决定 部114需要检索命题规则保存部102，取得符合所述条件的命题规则。

No.7的策略表示当检查结果保存部109保存有矛盾检查的检查结果601 时，取得与No.1的策略所表示的矛盾的规范605重复的命题规则，在决定表 上进行普通显示。应用这样的策略时，显示对象规则决定部114需要执行重复 检查部106，从检查结果保存部109取得该检查结果。另外，所述重复检查需 要将No.1的策略所表示的矛盾的规范605作为比较对象规则，将其它所有的 命题规则作为检查对象规则来实施。

图16是显示对象规则保存部115所保存的显示对象规则的例子。

显示对象规则一览1601由显示对象规则记述1602和显示方法1603构成。 显示对象规则1602表示显示对象规则决定部114根据从策略保存部111取得 的显示策略一览1501，从矛盾检查的检查结果601提取的显示对象规则。

例如，No.1的显示对象规则是根据显示策略一览1501中的No.1的策略， 将命题规则301和命题规则302的矛盾检查结果601中的矛盾的规范605作为 显示对象规则进行登录的结果。显示方法1603基于显示方法1504。

图17是表示显示对象规则决定的步骤例的流程图。

以下所示的处理通过决定表生成辅助/验证装置201所具备的CPU202在 存储器203中执行的程序来实现的。并且，该程序由进行以下所说明的各种动 作的代码构成。

CPU202通过执行显示对象规则决定部114，从检查结果保存部109取得 检查结果（步骤1701）。

显示对象规则决定部114参照取得的检查结果，从策略保存部所保存的显 示策略一览中取得由可选择策略设定部110挑选为满足策略适用条件1503、 且有效/无效属性1505为有效的策略（步骤1702）。

显示对象规则决定部114参照在步骤1702中取得的策略，为了根据策略 决定显示对象规则，判定是否需要和检查完毕的检查不同的追加检查。例如应 用显示策略一览1501中的No.7的策略时，需要追加进行重复检查。当判定为 需要追加检查时执行步骤1704。当判定为不需要追加检查时执行步骤1706（步 骤1703）。

显示对象规则决定部114根据需要的追加检查的种类来执行矛盾检查部 105、重复检查部106、未定义检查部107以及制约检查部108（步骤1704）。

显示对象规则决定部114从检查结果保存部109取得追加检查的结果（步 骤1705）。

显示对象规则决定部114根据在步骤1702中取得的策略，从取得的检查 结果中提取显示对象规则。有时候通过策略参照命题规则保存部102，从命题 规则保存部102所保存的命题规则中提取显示对象规则（步骤1706）。

显示对象规则决定部114将在步骤1706中提取出的显示对象规则登录在 显示对象规则保存部115中（步骤1707）。

图18是决定表部分显示/修正部116根据显示对象规则保存部115所保存 的显示对象规则进行显示的部分决定表的例子。

部分决定表1801是决定表部分显示/修正部116根据显示对象规则一览 1601进行显示的部分决定表。列1802表示根据显示对象规则一览1601中的 No.1的显示对象规则所显示的范围。根据显示方法1603，比其他的列更强调 地显示列1802。另外，条件项目1805是在步骤703以及步骤707中对检查对 象规则即命题规则301新追加的条件项目，因此被强调显示。

另外，部分决定表1801中，条件项目“国籍”是无关条件，被综合显示。 将解除了该综合显示的结果表示在部分决定表803中。列1804表示和列1803 同样的范围。或者也可以在部分决定表1801中将无关的条件项目“国籍”设 为不显示。

图19是通过决定表部分显示/修正部116接受修正输入而被修正的部分决 定表的例子。

修正完毕的部分决定表1901是修正了部分决定表1801的结果，包括被修 正的列1902。被修正的列1902是修正了列1802的结果，结果项目“补助金” 的值从“有交付”被修正为“没有交付”。

图20是修正完毕规则保存部118所保存的修正完毕规则的例子。

修正完毕规则一览2001由显示对象规则2002和其修正结果即修正完毕规 则2003构成。修正完毕规则生成部117从显示对象规则保存部115取得显示 对象规则一览1601，作为显示对象规则2002进行登录。另外，修正完毕规则 生成部117取得与显示对象规则2002对应的修正完毕的部分决定表，变换为 命题形式的规范并作为修正完毕规则2003进行登录。在先申请的专利文献2 中示出了将决定表形式的规范变换为命题形式的规范的方法。例如，修正完毕 规则一览2001中的No.1的显示处理规则是显示对象规则一览1601的No.1的 显示对象规则。该显示对象规则作为部分决定表1801的列1802被显示，且被 修正为修正完毕的部分决定表1901的列1902。因此，将列1902变换为命题 形式的规范“当“保险加入有无”是“已加入”且“保险缴纳额”是“2万日 元以上”时，“补助金”是“没有交付””，并作为修正完毕规则2003进行登录。

如上所述，可以提供一种软件规范开发辅助装置201，其对于表示软件规 范的决定表提供：命题形式的规范的输入手段；检查所述命题形式的规范间的 矛盾、重复、差分的手段；检查所述命题形式的规范的未定义规范的手段；检 查所述命题形式的规范是否满足制约的手段；根据所述检查的结果生成决定表 的手段；接受决定表的修正的手段；将修正完毕的决定表变换为命题形式的规 范的手段；将通过所述变换而得到的命题形式的规范和原来的命题形式的规范 进行置换的手段。