| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 1 绪论 | 第7-12页 |
| 1.1 研究问题 | 第7-8页 |
| 1.2 相关工作 | 第8-10页 |
| 1.3 本文工作 | 第10-12页 |
| 2 Alloy语言及其分析器 | 第12-17页 |
| 2.1 Alloy语言 | 第12-14页 |
| 2.2 Alloy分析器 | 第14-17页 |
| 3 群论的Alloy模型 | 第17-27页 |
| 3.1 群定义的建模 | 第17-20页 |
| 3.2 群基本性质的建模 | 第20-21页 |
| 3.3 子群性质的建模 | 第21-27页 |
| 4 群论定理的验证 | 第27-36页 |
| 4.1 验证平台及验证数据 | 第27-28页 |
| 4.2 群定义的等价性验证 | 第28-31页 |
| 4.3 群基本性质的验证 | 第31-33页 |
| 4.4 子群性质的验证 | 第33-36页 |
| 结论 | 第36-37页 |
| 参考文献 | 第37-39页 |
| 攻读硕士学位期间发表学术论文情况 | 第39-40页 |
| 致谢 | 第40页 |