Constness inference

It is common in software to have constants: values that, by design, never change at runtime. CertSAFE has language features to work with statically constant variables whose values are known to never change during the execution of a model. Statically constant values are indicated as gray wires in the diagram editor. I/O names connected to statically constant variables are drawn with a box around them. For example, the following diagram has a single output named “Foo” whose value is always TRUE:

ALT

Forward constness inference

Non-stateful components such as literals and arithmetic operations are called pure. CertSAFE can recognize calculations performed using only constant values and pure operations and perform constness inference to conclude that the results of such calculations must also be constant. For example, CertSAFE deduces that all of the values in this diagram are statically constant because only pure operations are involved:

ALT

Constness inference works automatically with custom components as well. Consider a custom component called “My Component” that is defined by the following diagram:

ALT

None of the values in this component are necessarily constant in all instances, but some of them will be constant if the input “A” is given a constant value. If we place a copy of My Component in a diagram that gives a constant value to “A”, CertSAFE will deduce that the output “B” must also be constant, while C is still non-constant due to the 1-frame delay:

ALT

CertSAFE deduces this based on information in the type signature inferred for My Component. If you mouse over My Component, CertSAFE displays the component’s type signature as follows:

ALT

Notice that the output “B” is inferred to be pure, while “C” is not. CertSAFE will mark a value as being constant if it is produced by a pure output of a component and all of the inputs of that component on which the output is dependent have been given constant values. Similarly, CertSAFE will mark a value as being pure if it is produced by a pure output of a component and all of the inputs of that component on which the output is dependent are pure.

CertSAFE also propagates constness information into instances when you are viewing a diagram in instance mode. In the case of the diagram shown previously, the instance of My Component is shown like this, illustrating how CertSAFE propagated the constness to determine that “A” and “B” are statically constant:

ALT

Backward constness inference

All of the examples shown to this point involved CertSAFE automatically deducing that values are constant by propagating constness from producers to consumers. However, CertSAFE also allows you to work in the other direction, by specifying that certain values must be constants and allowing the software to infer which inputs have to be constant to make that possible. You can mark an I/O of a diagram as requiring a constant value by setting the Constness annotation property of the I/O component. This is useful for making components that insist on constant values for certain inputs.

Suppose that, in the definition of My Component above, the “B” output had its constness annotation set to must be constant. CertSAFE would work backward and automatically determine that the input “A” requires a constant value:

ALT

If you then tried to use My Component with a non-constant value for “A”, CertSAFE would generate an error, saying that the component requires a constant value but the supplied value is not a constant. The same error would occur if you tried to set “C” to must be constant in the definition of My Component, since the output of the 1-frame delay cannot be statically constant.