我写了一小部分Haskell来弄清楚GHC如何证明对于自然数,你只能将偶数的一半:
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-}
module Nat where
data Nat = Z | S Nat
data Parity = Even | Odd
type family Flip (x :: Parity) :: Parity where
Flip Even = Odd
Flip Odd = Even
data ParNat :: Parity -> * where
PZ :: ParNat Even
PS :: (x ~ Flip y, y ~ Flip x) => ParNat x -> ParNat (Flip x)
halve :: ParNat Even -> Nat
halve PZ = Z
halve …继续观念:有没有可证明的现实世界语言？
我不了解你,但我厌倦了编写我无法保证的代码.
在询问了上述问题并得到了非凡的回应之后(谢谢大家!)我决定缩小我对Haskell的可证明,实用的方法的搜索范围.我选择哈斯克尔,因为它是真正有用的(也有许多 网页 框架为它写在纸上,这似乎是一个很好的基准)和我认为这是不够严格,在功能上,它可证明的,或者至少允许不变量的测试.
这就是我想要的(并且一直无法找到)
我想要一个可以查看Haskell函数的框架,添加,用psudocode编写:
add(a, b):
return a + b
- 并检查某些常量是否保持每个执行状态.我更喜欢一些正式的证据,但是我会满足于像模特检查员这样的东西.
在此示例中,不变量将是给定值a和b,返回值始终是总和a + b.
这是一个简单的例子,但我不认为这样的框架不可能存在.对于可以测试的函数的复杂性肯定会有一个上限(函数的10个字符串输入肯定会花费很长时间!)但这会鼓励更仔细地设计函数,并且与使用其他正式函数没有什么不同方法.想象一下,使用Z或B,当您定义变量/集时,您可以确保为变量提供尽可能小的范围.如果您的INT永远不会超过100,请确保将其初始化为!像这样的技术和正确的问题分解应该 - 我认为 - 允许对像Haskell这样的纯函数语言进行令人满意的检查.
我还没有 - 使用正式方法或Haskell非常有经验.让我知道我的想法是否合理,或者你认为haskell不合适？如果您建议使用其他语言,请确保通过"has-a-web-framework"测试,并阅读原始问题 :-)
testing haskell formal-verification formal-methods functional-programming
为什么计算机程序不能像数学陈述那样被证明？一个数学证明是建立在其他证明之上的,这些证据是从更多的证据和公理中建立起来的 - 我们认为这些真理是真实的.
计算机程序似乎没有这样的结构.如果您编写计算机程序,那么您如何能够获取以前经过验证的作品并使用它们来展示您的计划的真实性？你不能存在.此外,编程的公理是什么？这个领域的原子真理？
我对上面的内容没有很好的答案.但似乎软件无法被证明,因为它是艺术,而不是科学.你如何证明毕加索？
我在大学里接受过有关正式系统的教学,但我很失望,他们似乎并没有在真正的单词中使用它们.
我喜欢能够知道某些代码(对象,函数,等等)可以工作的想法,而不是通过测试,而是通过证明.
我确信我们都熟悉物理工程和软件工程之间不存在的相似之处(钢铁行为可预测,软件可以做任何事情 - 谁知道!),我很想知道是否有任何语言可以在真实的单词中使用(要求Web框架太多要问？)
我听说过像scala这样的函数式语言的可测试性.
作为软件工程师我们有什么选择？
java testing formal-verification functional-programming scala
考虑解决100名囚犯的标准策略和灯泡问题.这是我在Dafny模拟它的尝试:
method strategy<T>(P: set<T>, Special: T) returns (count: int)
requires |P| > 1 && Special in P
ensures count == (|P| - 1)
decreases *
{
count := 0;
var I := {};
var S := {};
var switch := false;
while (count < (|P|-1))
invariant count <= (|P|-1)
invariant count > 0 ==> Special in I
invariant Special !in S && S < P && S <= I && I <= P
decreases *
{ …我在大学里瞥见了Hoare Logic.我们做的很简单.我所做的大部分工作都证明了由while循环,if语句和指令序列组成的简单程序的正确性,但仅此而已.这些方法似乎非常有用!
工业上使用的正式方法是否广泛？
这些方法是否用于证明任务关键型软件？
一个纯粹的 功能类似于一个数学函数,在那里与"现实世界",也不副作用没有交互的功能.从更实际的角度来看,这意味着纯函数不能:
所有这些限制使得更容易推理纯函数而不是非纯函数.然后,大多数函数应该是纯函数,以便程序可以减少错误.
在像Haskell这样的庞大类型系统的语言中,如果函数是纯粹的或者不是纯粹的,读者可以从一开始就知道,使得连续阅读更容易.
在Python中,这些信息可以由@pure放在函数顶部的装饰器模拟.我也希望那个装饰器实际上做一些验证工作.我的问题在于这种装饰器的实现.
现在我只是看一下流行语的功能的源代码,如globalor random或print抱怨,如果找到其中一个.
import inspect
def pure(function):
source = inspect.getsource(function)
for non_pure_indicator in ('random', 'time', 'input', 'print', 'global'):
if non_pure_indicator in source:
raise ValueError("The function {} is not pure as it uses `{}`".format(
function.__name__, non_pure_indicator))
return function
然而,感觉就像一个奇怪的黑客,根据你的运气可能会或可能不会工作,你能帮我写一个更好的装饰？
python formal-verification metaprogramming decorator purely-functional
我正在尝试在运算符和运算符上为我的自定义数据类型创建一个Semigroup和VerifiedSemigroup实例:Bool&&||
%case data Lógico = Cierto | Falso
(&&) : Lógico -> Lógico -> Lógico
(&&) Cierto Cierto = Cierto
(&&) _ _ = Falso
(||) : Lógico -> Lógico -> Lógico
(||) Falso Falso = Falso
(||) _ _ = Cierto
所以我先制作一个命名实例为Semigroup在 &&运营商:
-- Todos
instance [TodosSemigroup] Semigroup Lógico where
(<+>) a b = a && b
但在制作VerifiedSemigroup实例时,如何告诉Idris使用TodosSemigroup实例Lógico？ …
formal-verification named-instance typeclass idris semigroup
我试图在Coq中证明以下引理:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> [] \/ b <> []) -> a ++ b <> [].
现在我当前的策略是破坏一个,在打破分离之后,理想情况下我可以说,如果一个<> []那么a ++ b也必须<> [] ......这就是计划,但我似乎无法通过类似于第一个"a ++ b <> []"的子目标,即使我的上下文明确指出"b <> []".有什么建议？
我还查看了很多已有的列表定理,并没有找到任何特别有用的东西(减去app_nil_l和app_nil_r,对于某些子目标).