基于COQ的有限域GF(2n)的形式化研究

有限域GF(2n)是多种安全关键性算法的基础,包括AES加密算法、椭圆曲线加密和感染函数掩码等。相关资料表明,有限域上的运算因为自身的复杂性而容易出错,从而导致系统问题。基于测试和基于模型检测的验证方法只能在n固定的特定有限域上进行验证,而且计算量往往超出计算机的能力。基于交互式定理证明器的形式化验证为有限域性质的通用验证提供了可能性,但这方面的工作难度较大。已有研究主要针对有限域的抽象性质进行形式化验证,但计算机领域更关心的是有限域的构造性定义及相关性质的验证。针对这些问题,借助定理证明器COQ,建立了有限域GF(2n)并给出了其基本运算的构造性定义,同时对一组与有限域有关的基本性质进行了形式化验证,包括有限域加法基本性质的验证、多项式乘法基本性质的验证等,其中多项式乘法是有限域乘法的基础。这项工作为有限域的完整的形式化及基于有限域的算法的形式化验证奠定了基础。

拓宽思路提高组合体识图能力

识图过程是一个综合思维的过程,从分析原因入手,在教学实践中采用各种教学方法,促使学生掌握系统科学的识图方法,培养学生善于观察的能力,注重学生主体性的发挥,提高学生空间思维能力,全面提高学生识图能力。

面向全体因材施教——在制图教学中实施分层教学的探索与实践

在制图课程教学实践中应实行分层教学,应充分考虑学生的个体差异,将教师的个别辅导、分组辅导、集体辅导与学生的自学、分组学、全体学有机地统一起来,有助于培养学生学习兴趣,充分发挥学生学习的自主性,变"要我学"为"我要学"让学生的个性和特长得到充分的发展,更好地完成制图课程的教学目标。