期刊文献+
共找到4篇文章
< 1 >
每页显示 20 50 100
Trie+结构函数式建模、机械化验证及其应用
1
作者 左正康 柯雨含 +3 位作者 黄箐 王玥坤 曾志城 王昌晶 《软件学报》 EI CSCD 北大核心 2024年第9期4242-4264,共23页
Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基... Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.Nipkow等人给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,基于索引即键值的思想提出了Trie+结构,相较于传统的索引与键值分开存储的结构能减少50%的存储空间,大大提高了空间利用率.并且,对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证,保证操作的正确性和可靠性.进一步,提出一种匹配算法的通用验证规约,旨在解决一系列的匹配算法正确性验证问题.最后,基于Trie+结构与匹配算法通用验证规约,建模和验证了函数式中英文混合多模式匹配算法,发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug.该Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中,有一定的理论和应用价值. 展开更多
关键词 Trie+ 函数式建模 机械化验证 匹配算法
下载PDF
基于最大半环的DP问题函数式建模与验证
2
作者 王唱唱 游珍 +1 位作者 孙欢 王昌晶 《江西师范大学学报(自然科学版)》 CAS 北大核心 2024年第3期294-300,310,共8页
针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的... 针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的基于最大半环的函数式建模算法与Wimmer定义的递归函数结果进行等价性验证,从而保证了函数式建模算法的正确性;最后通过对lcs问题案例分析,验证了该方法的可行性和有效性. 展开更多
关键词 DP问题 最大半环 函数式建模 验证
下载PDF
Implicit modeling of complex orebody with constraints of geological rules 被引量:13
3
作者 De-yun ZHONG Li-guan WANG +1 位作者 Lin BI Ming-tao JIA 《Transactions of Nonferrous Metals Society of China》 SCIE EI CAS CSCD 2019年第11期2392-2399,共8页
To dynamically update the shape of orebody according to the knowledge of a structural geologist’s insight,an approach of orebody implicit modeling from raw drillhole data using the generalized radial basis function i... To dynamically update the shape of orebody according to the knowledge of a structural geologist’s insight,an approach of orebody implicit modeling from raw drillhole data using the generalized radial basis function interpolant was presented.A variety of constraint rules,including geology trend line,geology constraint line,geology trend surface,geology constraint surface and anisotropy,which can be converted into interpolation constraints,were developed to dynamically control the geology trends.Combined with the interactive tools of constraint rules,this method can avoid the shortcomings of the explicit modeling method based on the contour stitching,such as poor model quality,and is difficult to update dynamically,and simplify the modeling process of orebody.The results of numerical experiments show that the 3D ore body model can be reconstructed quickly,accurately and dynamically by the implicit modeling method. 展开更多
关键词 three-dimensional geomodeling implicit modeling radial basis function structural anisotropy geological rules
下载PDF
Linux-based Platform for Open Architecture Controller and Its Modular Developing Method
4
作者 迟永琳 王宇晗 +1 位作者 吴祖育 蔡建国 《Journal of Donghua University(English Edition)》 EI CAS 2003年第2期107-111,共5页
Linux-based Platform for Open Architecture Controller ( POAC ), a new open architecture controller and its modular developing method are discussed. POAC divides the application software of controller into the developi... Linux-based Platform for Open Architecture Controller ( POAC ), a new open architecture controller and its modular developing method are discussed. POAC divides the application software of controller into the developing system and the application system. In the developing system, PAOC abstracts a series of function modules with unified data interface and function interface. In the application system, POAC defines the model of the architecture module, realizing the interoperability and interchangeability between the architecture modules. The modular developing method entities the users to make up an application system with some architecture modules, which consist of a set of function modules. The modular developing method decreases the developing time from the standard of controller architecture to the product. 展开更多
关键词 Open architecture controller Function Module Architecture Modules Modular developing method
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部