Ada_Ru форум

Обсуждение языка Ада

Объясните логику quantified expression применительно к пустым массивам

Оставить новое сообщение

Сообщения

KsiCom
Объясните логику quantified expression применительно к пустым массивам
2012-08-17 13:39:35

Возьмём простую программу:

 

with Ada.Text_IO; use Ada.Text_IO;

procedure Alfa is

   type zzz is array (Integer range <>) of Integer;

   A : zzz (1 .. 10) := (others => 0);

   B : zzz (10 .. 1) := (others => 0);

   T : Boolean := False;

begin

   T := (for all E of A => E = 1);

   Put_Line (Boolean'Image (T));

   --  T = FALSE All Ok.

   T := False;

   T := (for all E of B => E = 1);

   Put_Line (Boolean'Image (T));

   --  ??? T = TRUE ???

   T := False;

   T := (for all i in B'Range => B (i) = 1);

   Put_Line (Boolean'Image (T));

   --  ??? T = TRUE ???

end Alfa;

 

Почему для пустого массива выражение возвращает True? Почему не генерится exception ну или хотя бы False?

Это ещё простой случай. А если размерность массива динамическая и ещё такое выражение засунуто куда-нибудь в Pre/Post condition, то совсем грустно становится.

Почему для пустого массива выражение возвращает True? Почему не генерится exception ну или хотя бы False?

Это соответствует общепринятому соглашению для квантора всеобщности пустого множества. Напомню, выражение ∀х∈∅:Р(х) является истинным для любого выражения Р(х).

Это ещё простой случай. А если размерность массива динамическая и ещё такое выражение засунуто куда-нибудь в Pre/Post condition, то совсем грустно становится.

Не нужно грустить, нужно просто записать условие вот так:

T := B'First in B'Range and then (for all E of B => E = 1);

ВФ

Новое сообщение:
Страницы: 1

Чтобы оставить новое сообщение необходимо Зарегистрироваться и Войти