摘要：动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP(minimalistic imperative programming language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG(verification condition generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.

摘要：随着虚拟现实技术的发展,鼠标和键盘等传统输入模态已经难以满足沉浸式虚拟现实交互需求,如何使用自然交互方式来满足沉浸式交互任务日益成为研究热点.为了实现自然高效的人机交互,该文首先分析各种单模态交互方式的优缺点,并基于神经科学和运动学的角度划分视线转移;其次,结合头动的稳定性与眼动的高效性以及头眼协调特征设计了一个头眼协调交互模型,通过多模态相互作用减少Midas误触和识别用户意图;最后,针对虚拟现实的目标选择任务进行模态对比实验.实验结果表明:与传统交互模态相比,该交互模型具有更高的精度、更快的时间效率和更高的自然度.

摘要：针对传统的脚本建模存在语言机制复杂繁琐、开发效率不高、可靠性难保证、建模阶段和交互阶段相互独立等问题,基于分划与递推(PAR)及其Apla抽象程序设计语言,设计与原Apla语言融合的虚拟现实建模语言机制。开发的Apla→MAXScript自动生成系统可以将抽象Apla程序转换成MAXScript脚本,并借助3DSMax来实现三维建模。Apla建模机制采用直接重用MAXScript修改器API方式,既大幅度简化了重构的工作量,又延续了Apla语言抽象程度高特征,便于对Apla建模程序进行形式化推导和正确性验证。最后通过案例证明了Apla建模语言及其工具能够提高三维建模的精细度、可靠性及开发效率。

摘要：设计并实现了一个PAR方法的在线自学系统.利用Web服务(Web Service)和多媒体数据库技术,将使用PAR方法开发算法程序设计的基本概念、算法设计语言Radl、抽象程序设计语言Apla以及设计和推导算法程序的方法学形象生动地呈现给学习者.最后介绍了利用算法程序设计支撑平台生成可执行算法程序的过程,以及该算法程序运行产生的结果.

摘要：随着信息技术在各大领域的广泛应用,产生的多媒体数据所占比例越来越大,对多媒体数据处理的需求也越来越多,高级程序设计语言支持多媒体数据处理的功能也变得尤为重要.采用模型驱动的思想,在支持模型驱动软件开发PAR平台的Apla→Java程序自动生成系统中,扩充对多媒体数据处理的功能,并提出多媒体数据处理机制和Apla中基于关系代数的文本处理机制自然融合,包含了对多媒体数据处理的Apla语言程序,可以通过Apla→Java程序自动生成系统自动转换成等价的Java程序,使得Apla语言具有对多媒体数据处理的能力.

摘要：随着电子商务和金融软件应用日益广泛,提高这类软件系统的可靠性和安全性就显得特别重要。虽然能够提高这类软件可靠性的事务处理技术早在数据库管理系统中普遍使用,近几年在Java软件开发环境中也新增了事务处理接口JTA,但是在基于模型驱动架构设计的建模语言中嵌入事务处理机制的成功案例尚不多见。论文在已有体现模型驱动软件架构思想的PAR方法和PAR平台中,融入抽象事务处理机制,并使用融入了事务处理机制的PAR平台及其建模语言开发了具有事务处理功能的金融软件模型,通过PAR平台的模型自动转换工具生成了Java和SQL程序。实验证明融入了事务处理机制的PAR方法和PAR平台具有建模简单、实用,软件开发效率高,便于形式化推导和证明等特点。

摘要：虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得十分庞大和复杂,涉及许多多媒体数据。传统软件开发方法和程序设计技术侧重于处理文本数据,显然不能满足开发虚拟现实软件的需要。试图以所在团队研发成功的PAR方法和PAR平台为基础,根据虚拟现实软件系统的特征,探寻虚拟现实软件系统开发的新方法,进一步扩充和完善PAR平台中已有多媒体处理技术、形式化建模技术和C#等高级语言程序自动生成系统。

摘要：为应对传统计算机算法教学中理论知识存在逻辑性强、抽象程度高、教学与实验脱节、缺乏交互性等现实问题,本文借助虚拟现实技术,基于江西知名旅游胜地庐山的三维场景,使用Unity3D引擎设计图算法虚拟仿真系统。该系统实现5种图算法的仿真实验过程,每种图算法均提供“自动展示”和“用户交互”这2种运行模式,还提供用户进入景点(对应图的结点)分场景的自由控制视角浏览庐山景观的功能;同时,探讨本虚拟仿真系统存在的理论问题,并给出解决这些问题的关键技术和实施方案;最后,通过Prim最小生成树算法验证本虚拟仿真系统的实用性和灵活性。与传统的算法讲授、个性化问题驱动教学方式相比,本文设计的图算法虚拟仿真系统具有趣味性、交互性、沉浸性,既能激发学生学习的探索性和主动性,又为算法与数据结构课程提供了一种新的教学和实验方法。