这个C程序如何工作？
main(_){_^448&&main(-~_);putchar(--_%64?32|-~7[__TIME__-_/8%8][">'txiZ^(~z?"-48]>>";;;====~$::199"[_*2&8|_/64]/(_&2?1:8)%8&1:10);}
它按原样进行编译(测试gcc 4.6.3).它打印编译时的时间.在我的系统上:
!! !!!!!! !! !!!!!! !! !!!!!!
!! !! !! !! !! !! !! !!
!! !! !! !! !! !! !! !!
!! !!!!!! !! !! !! !! !! !!!!!!
!! !! !! !! !! !! !!
!! !! !! !! !! !! !!
!! !!!!!! !! !! !! !!!!!!
资料来源:sykes2 - 一行中的一个时钟,sykes2作者提示
一些提示:默认情况下没有编译警告.编译时-Wall,会发出以下警告:
sykes2.c:1:1: warning: return type defaults to ‘int’ [-Wreturn-type]
sykes2.c: In function ‘main’:
sykes2.c:1:14: warning: value …当我apply (rule)在apply-script中使用时,通常会选择适当的规则.这同样适用于proof结构化证明.我在哪里可以学习/查找所用规则的名称？
让我们假设我想要显示以下引理
lemma "? A; B; C ? ? D"
我得到了目标
1. A ? B ? C ? D
但是,我不需要B.我怎样才能将目标转移到类似的东西上
1. A ? C ? D
我不想改变原始lemma陈述,只是改变申请风格的当前目标.
当我导入带有定义常量(用于递归函数或定义)f的理论文件时,如何在当前理论文件中隐藏这样的常量？换句话说,我想确保它f是一个自由变量.我不想更改导入的文件.
这个问题扩展了如何隐藏定义的常量的问题。
我进口的理论A，B以及C，也许在将来也D，E......所有的理论定义一个函数f。我想f在不改变导入的理论的情况下隐藏我当前理论中的定义。当我写term f我得到A.f。当我添加hide_const (open) f到我当前的理论时，A.f是隐藏的，但现在我得到B.f了f. 我怎样才能完全隐藏f？我需要类似的东西(hide_const (open) f)+。
对于AFP条目Dijkstra's Shortest Path Algorithm，证明大纲和证明文件都不存在 *。不幸的是，我没有找到在IsaMakefile本地构建这些文档的工具。获取这些文件的最佳方式是什么？
另一个问题，由于Dijkstra.thy依赖于许多其他理论，有没有办法更快地加载所有内容？
*)现在已修复。
这个问题涉及使用Isabelle/HOL定理证明器生成代码.
当我导出distinct列表上的函数的代码时
export_code distinct in Scala file -
我得到以下代码
def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
case (Nil, y) => false
case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y)
}
def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match {
case Nil => true
case x :: xs => ! (member[A](xs, x)) && distinct[A](xs)
}
此代码具有二次运行时.有更快的版本吗？我想到了"~~/src/HOL/Library/Code_Char"在我的理论开头导入字符串并建立列表的高效代码生成之类的东西.更好的实现distinct方法是在O(n log n)中对列表进行排序,并迭代列表一次.但我猜一个人可以做得更好吗？
无论如何,是否有更快的实现distinct和可能的其他功能Main？