c - 定义非零整数结构

Question

假设我们想要定义整数除法以排除被零除。有可能这样做吗？我想要看起来像这样的东西:

#include <stdio.h>
#include <assert.h>

/* Define a structure intn0. */
typedef struct intn0 intn0;

struct intn0{
    int x;
    /* assert(x != 0); */
};

int div(int a, intn0 b){
    return a / b.x;
};

显然，这是行不通的。有没有一种方法可以在结构级别上执行这种断言，比如说，为了定义一个除法函数，以便对于所有有效输入(即正确类型的输入)，我们可以保证它会生成有效输出而无需错误且没有垃圾？

如果您不能在 C 中执行此操作，那么哪种语言允许这种抽象(最好是类似于 C 而不是 Haskell 之类的东西)？

Answer 1

Is there a way to perform this sort of assertion on the structure level, say,

断言对应于(启用时)可执行代码。您不能将断言嵌入到 C 中的数据结构中，尽管您可以在 Java 或 C++(例如)中这样做，方法是将类的成员设为私有(private)并使用测试有效性的代码保护所有设置它们的方法(由类定义) ) 的建议值。正如@RSahu 所观察到的，您可以在 C 中做类似的事情，尽管该语言没有提供实际强制执行它的方法。

但是，在某些情况下，可以定义一个数据结构，该数据结构不代表您不希望它代表的值。例如:

/*
 * Represents a non-zero integer between -(UINT_MAX+1) and (UINT_MAX+1),
 * inclusive; has no representation for zero.
 */
struct intn0 {
    _Bool is_negative;
    unsigned n_less_one;
};

for the purpose of defining a division function such that for all valid inputs (i.e. inputs of the correct type), we can guarantee it will generate a valid output without error and without garbage?

具有上述结构类型的整数除法可能如下所示:

int div(int a, struct intn0 b){
    return (b.is_negative ? -1 : 1) * (a / ((long long) b.n_less_one + 1));
};

假设 long long 类型足够大以表示 UINT_MAX + 1，它永远不会被零除，并且始终会为每个值产生一致且合理的结果可能的一对参数。如果除法语义不是您想要的，那么我相信您可以调整它们以适应。