--- ai12s/ai12-0438-1.txt 2022/05/07 06:14:18 1.2 +++ ai12s/ai12-0438-1.txt 2022/06/14 23:39:33 1.3 @@ -106,46 +106,46 @@ Modify A.18.2(237.7/5): - If a stable vector is declared without specifying Base, the object - {has to}[must] be initialized. The initializing expression of the stable vector, - typically a call on To_Vector or Copy, determines the Length of the vector. - The Length of a stable vector never changes after initialization. + If a stable vector is declared without specifying Base, the object{is + necessarily}[must be] initialized. The initializing expression of the stable + vector, typically a call on To_Vector or Copy, determines the Length of the + vector. The Length of a stable vector never changes after initialization. {AARM Proof: Initialization is required as the type is indefinite, see 3.3.1.} Modify A.18.3(151.6/5): - If a stable list is declared without specifying Base, the object {has to}[must] - be initialized. The initializing expression of the stable list, typically a - call on Copy, determines the Length of the list. The Length of a stable list - never changes after initialization. + If a stable list is declared without specifying Base, the object {is + necessarily}[must be] be initialized. The initializing expression of the stable + list, typically a call on Copy, determines the Length of the list. The Length + of a stable list never changes after initialization. {AARM Proof: Initialization is required as the type is indefinite, see 3.3.1.} Modify A.18.4(75.6/5): - If a stable map is declared without specifying Base, the object {has to}[must] - be initialized. The initializing expression of the stable map, typically a call - on Copy, determines the Length of the map. The Length of a stable map never - changes after initialization. + If a stable map is declared without specifying Base, the object {is + necessarily}[must be]initialized. The initializing expression of the stable + map, typically a call on Copy, determines the Length of the map. The Length + of a stable map never changes after initialization. {AARM Proof: Initialization is required as the type is indefinite, see 3.3.1.} Modify A.18.7(98.18/5): - If a stable set is declared without specifying Base, the object {has to}[must] - be initialized. The initializing expression of the stable set, typically a - call on Copy, determines the Length of the set. The Length of a stable set - never changes after initialization. + If a stable set is declared without specifying Base, the object {is + necessarily}[must be] initialized. The initializing expression of the stable + set, typically a call on Copy, determines the Length of the set. The Length + of a stable set never changes after initialization. {AARM Proof: Initialization is required as the type is indefinite, see 3.3.1.} Modify A.18.10(218.6/5): - If a stable tree is declared without specifying Base, the object {has to}[must] - be initialized. The initializing expression of the stable tree, typically a - call on Copy, determines the Node_Count of the tree. The Node_Count of a - stable tree never changes after initialization. + If a stable tree is declared without specifying Base, the object {is + necessarily}[must be] initialized. The initializing expression of the stable + tree, typically a call on Copy, determines the Node_Count of the tree. The + Node_Count of a stable tree never changes after initialization. {AARM Proof: Initialization is required as the type is indefinite, see 3.3.1.}

Questions? Ask the ACAA Technical Agent