这个标准是否证明Y无限递归地调用X？

Question

#include <stdint.h>
typedef int(*ptr)(); 

int X(ptr P, ptr I)  
{
  P(I); 
  return 0; 
}

int Y(ptr P)  
{
  X(P, P);
  return 1; 
}

int main()
{
  X(Y, Y);
}

Y 使用与调用者相同的参数来调用其调用者，这一事实是否证明 Y 正在无限递归中调用 X？

如果我们添加 Y 和 X 都没有任何条件分支指令这一事实呢？

Answer 1

由于 main 不 use 返回值（其他函数也不使用），因此用

X

替换

Y

和

void

的返回类型（并删除

return

语句）是否有效？ ）？这将是证明的第一步（我相信这是可能的）。 – 克雷格·埃斯蒂

是的，这是有效的。 – 波尔科特

警告：我以前从未做过正式证明，但我会尝试使用我理解的代码等效替换。

---

步骤总结：

1. 原代码
2. 将返回类型转换为 void 并删除返回语句
3. 因为对 X 的所有调用对每个参数都使用相同的值， 将 X 转换为使用单个参数
4. 将 X 内联到 Y 中
5. 将所有 Y 替换为 X，因为它们相同并删除 Y
6. 由于 X 是用参数 X 调用的（仅在 main 中），因此将 X 中 X 与 X 的参数（即 P --> X）
7. 由于 X 不再依赖于其参数，因此删除该参数

---

// step1 -- original code

#include <stdint.h>
typedef int (*ptr) ();

int
X(ptr P, ptr I)
{
    P(I);
    return 0;
}

int
Y(ptr P)
{
    X(P, P);
    return 1;
}

int
main()
{
    X(Y, Y);
}

---

// step2 -- convert return types to void and remove return statements

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P, ptr I)
{
    P(I);
}

void
Y(ptr P)
{
    X(P, P);
}

int
main()
{
    X(Y, Y);
}

---

// step3 -- because all calls to X use the same value for each argument,
// convert X to use a single argument

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    X(P);
}

int
main()
{
    X(Y);
}

---

// step4 -- inline X into Y

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

void
Y(ptr P)
{
    P(P);
}

int
main()
{
    X(Y);
}

---

// step5 -- replace all Y with X because they are the same and remove Y

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    P(P);
}

int
main()
{
    X(X);
}

---

// step6 -- since X is called (only in main) with argument X, replace the
// argument to X in X with X (i.e. P --> X)

#include <stdint.h>
typedef void (*ptr) ();

void
X(ptr P)
{
    X(X);
}

int
main()
{
    X(X);
}

---

// step7 -- since X no longer depends on its argument, remove the argument

#include <stdint.h>
typedef void (*ptr) ();

void
X(void)
{
    X();
}

int
main()
{
    X();
}

---

在步骤(7)中，

main

调用

X

。而且，

X

只是自称[无限]。