霍尔逻辑是一种众所周知的基于一阶逻辑对命令式程序的行为进行推理和验证的形式系统。然而，使用霍尔逻辑对于存在指针和动态数据结构的命令式程序进行推理和验证是一件比较困难的事情。主要问题在于:1)一阶逻辑没有表达指针变量非别名的原语，在程序分析与验证时必须考虑所有的别名模式，2）当牵涉到内存分配和释放操作时，需要对指针变量所处的论域进行扩充或限制，而一阶逻辑不具备改变变量所处的论域的能力。为了克服霍尔逻辑的上述缺陷，Reynolds、OHearn等人在2000年左右提出了分离逻辑。分离逻辑通过引入分离算子克服了霍尔逻辑的上述不足，使得能够以比较自然的方式来描述程序计算过程中内存和动态数据结构的性质，从而简化了对含有指针和动态数据结构的命令式程序的验证工作。而且，分离逻辑能够支持局部推理，可以将推理集中在程序执行过程中所访问的内存片段上，然后再通过框架规则(Frame rule)将推理扩展到程序的全局状态。　　在使用分离逻辑对含有动态数据结构的命令式程序进行验证时，一般引入归纳谓词来对动态数据结构进行抽象表示，而且程序验证问题最终归结为两个分离逻辑公式的蕴涵问题。由于含有归纳谓词的分离逻辑的蕴涵问题一般是不可判定的，目前的大多数基于分离逻辑的工具只提供了不完备的判定算法。　　在本文中，我们定义了带线性可组合归纳谓词与数据约束的分离逻辑的一个子集，使得可以在统一的框架下同时对线性数据结构的形状性质（即单链表、双链表、带尾指针的单双链表）与数据性质（比如有序性和长度约束）进行描述。我们针对该子集的可满足性问题与蕴涵问题提供了完备的判定算法。我们将该子集的可满足性问题归结为整数域上的线性算术公式的可满足性问题，然后交给目前主流的SMT求解器求解。对于蕴涵问题，我们将分离逻辑公式用图来表示，然后将两个逻辑公式的蕴涵问题转化为它们的图表示之间的某种图同态问题。最后，我们将我们的判定算法进行了实现，开发了原型工具，进行了相关实例研究。