标签: formal-semantics

我一直在阅读关于形式验证的文章，基本点是它需要一个正式的规范和模型来使用。然而，许多来源将静态分析归类为形式验证技术，有些提到抽象解释并提到它在编译器中的使用。所以我很困惑 - 如果没有模型的正式描述，这些如何进行形式验证？
编辑：我发现的一个来源是：

静态分析：根据预定义的抽象（有时可以由用户自动/手动定制）从程序文本中自动计算抽象语义

那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。

另外，在没有形式验证的情况下可以进行静态分析吗？例如，SonarQube 真的执行形式化方法吗？

许多编程语言共享通用甚至相当普遍的功能.例如,如果您比较Java,VB6,.NET,PHP,Python,那么您会发现常见的功能,如控制结构,数字和字符串操作等.

在元语言(或语言不可知)级别定义这些功能已经做了些什么？

UML在各个方面都提供了软件的描述性参考,但现实世界的重点似乎是数据处理.UML是否相关？

我不是在问"为什么我们没有一种语言可以取代目前的过多." 我们需要许多不同的工具(至少在这个时代).

我不是要求所有语言都适合模板 - 汇编与编译语言的不同使得这种语言不可行(有些人称HTML为语言,尽管我不这样做).任何尝试都将以适当狭窄的范围开始.根据这一点,我不希望该模型甚至涵盖一个完整有效的小选择.

然而,我希望这样的模型可以用于从一种语言转换到另一种语言(目标有限 - 思考jist翻译).

我是一名(理论)计算机科学专业的学生,​​因此研究编程语言的语义是我研究的主题之一(维基百科).

我使用CSS玩了很多,并且对盒子定位规则有了合理的理解.(如果你告诉我创建一个具有特定布局的页面,我通常会想到正确的方法和适用的CSS规则.)

为CSS盒子定位规则提供某种形式语义会很酷,但是在搜索网络一段时间之后,我找不到任何有用的东西.

我大多只是简单地结束了CSS规范,这些规范被格式化为具有伪算法的长文本(不是最大的读物 - 我还没有花很多精力阅读这些规范).

没有人试图将这个"理论"形式化为某种数学模型,比规范提供的更严格吗？我不是在寻找完整或确定的东西,但如果至少应该以正式的方式对盒子的定位方式进行建模,那么它肯定会是整洁的(并且很有用!).

有谁知道这样的研究？

想象一下

exp(49/200)+(x-49/200)

我想作为函数"roundn"的参数传递任何不是加法或减法的操作所以我的表达式变成了

roundn(exp(roundn(49/200, n)), n) + (x - roundn(49/200, n)

我想要操纵的表达是这样的:

exp(49/200)+exp(49/200)*(x-49/200)+1/2*exp(49/200)*(x-49/200)^2+1/6*exp(49/200)*(x-49/200)^3+1/24*exp(49/200)*(x-49/200)^4+1/120*exp(49/200)*(x-49/200)^5+1/720*exp(49/200)*(x-49/200)^6+1/5040*exp(49/200)*(x-49/200)^7+1/40320*exp(49/200)*(x-49/200)^8+1/362880*exp(49/200)*(x-49/200)^9+1/3628800*exp(49/200)*(x-49/200)^10+1/39916800*exp(49/200)*(x-49/200)^11