Safe Objective Language

[valexey_u]

Там к WHILE приписывается ограничитель максимального числа итераций. Типа, "защита от зависания" для встроенки.
Так же защита от глубины рекурсии

Вау! Я же в том же направлении копал, и пришел к примерно тем же выводам (правда признал их слишком корявыми :-) ). Это попытка избавиться от полноты по Тьюрингу (ибо она нафиг не уперлась в подавляющем большенстве задач и алгоритмов) с её замечательной задачей о останове. В не Тьюринг-полных языках, вообще говоря, проблем со, скажем, выходом за границы массива может и не быть (и никаких рантайм проверок).

Ну и как побочная фича - можно автоматически оценить сверху время выполнения/трудоемкость любых библиотечных функций (даже если там внутри что-то жирное-жирное, вроде кодирования h264).

Я пробежал "талмуд" за 20 минут, отметил корреляции со своим пониманием в плане управления памятью.

Да, надо будет пробежаться тоже. Правда мне не слишком нравится тон которым оно написано. Слишком поучительный :-) Я бы хотел прочесть просто спеку + отдельно rationale.

[vlad]

Несмотря на "дремучесть" в ряде моментов (типа выходов из вложенных циклов и ограничения итераций - хотя хз, может быть, для встроенки такое ограничение от зависания тоже имеет смысл), там накопана "траншея" в правильную сторону - там, где касается указателей и управления памятью.

Почитал про указатели. Ничего интересного там не накопано. Сильные/слабые указатели - давно известный и применяемый паттерн. Описание попыток контроля циклических ссылок со стороны компилятора - не выдерживает проверки на абстрактных типах. Само по себе счетчики ссылок - всегда были только от бедности. Проблема ненулевых указателей никак не обозначена. Вобщем буков много, но все равно бледно.

[DIzer]

Это попытка избавиться от полноты по Тьюрингу (ибо она нафиг не уперлась в подавляющем большенстве задач и алгоритмов) с её замечательной задачей о останове. В не Тьюринг-полных языках, вообще говоря, проблем со, скажем, выходом за границы массива может и не быть (и никаких рантайм проверок).

Опять использование  понятия "полноты по Тьюрингу" - совершенно не коррелирующее с моим и проблемой(в  моем понимании)... - вопрос.. как вы избавитесь от проверки  если верхняя граница массива вводится ДИНАМИЧЕСКИ (во время выполнения) - с консоли...

[DIzer]

то есть самое простое:

Код: [Выделить]

var A:array [1..10] of real;
     i:integer;
Begin
readln(i);
a[i]:=Pi; - //вопрос - как  обойтись здесь проверкой времени компиляции, предложите процесс на Тюринг - неполном ЯП - основываясь только на этих данных  ;)
writeln(a[i]);
end.


[Geniepro]

Примерно так:

Код: [Выделить]

type ArrSize is new Integer range 1 .. 10;

with Ada.Text_IO; use Ada.Text_IO;

package ArrSize_IO is new Integer_IO(ArrSize);

arr: array (ArrSize) or Real;
i: ArrSize;

begin
    Get(i);
    a(i):=Pi;
    Put(a(i));
end

[DIzer]

Примерно так:

Код: [Выделить]

type ArrSize is new Integer range 1 .. 10;

with Ada.Text_IO; use Ada.Text_IO;

package ArrSize_IO is new Integer_IO(ArrSize);

arr: array (ArrSize) or Real;
i: ArrSize;

begin
    Get(i);
    a(i):=Pi;
    Put(a(i));
end

Не понял.. как вы на этапе КОМПИЛЯЦИИ определите возможную ошибку... - в вашем коде замаскированная проверка ВРЕМЕНИ ВЫПОЛНЕНИЯ

[DIzer]

вообще говоря меня насторожило
http://oberspace.dyndns.org/index.php?action=post;quote=10797;topic=384.0;last_msg=10865 - но тогда я подумал, что Алексей гнусно стебается
над jordan'ом...

[valexey_u]

вообще говоря меня насторожило
http://oberspace.dyndns.org/index.php?action=post;quote=10797;topic=384.0;last_msg=10865 - но тогда я подумал, что Алексей гнусно стебается
над jordan'ом...

то есть ты намекаешь таки, что всетаки можно? :-)

[DIzer]

вообще говоря меня насторожило
http://oberspace.dyndns.org/index.php?action=post;quote=10797;topic=384.0;last_msg=10865 - но тогда я подумал, что Алексей гнусно стебается
над jordan'ом...

то есть ты намекаешь таки, что всетаки можно? :-)

я намекаю на то что не очень хорошо стебаться над начинающими.. - это порождает  ложное чувство  безнаказанности ... и может вернуться в неожиданных ситуациях.... а по вопросу - я не знаю такого способа.. для незамкнутой системы  (вот и хотел просветится от "профессионалов" поднаторевших  в данных вопросах) 

[Geniepro]

Не понял.. как вы на этапе КОМПИЛЯЦИИ определите возможную ошибку... - в вашем коде замаскированная проверка ВРЕМЕНИ ВЫПОЛНЕНИЯ

Часть сообщения не отправилась из-за невнимательности, наверное. И ваще правильнее, наверное, так (компилятора под рукой нет что бы проверить):

Код: [Выделить]

type ArrSize is new Integer range 1 .. 10;

with Ada.Text_IO; use Ada.Text_IO;

package ArrSize_IO is new Integer_IO(ArrSize);

arr: array (ArrSize) or Real;
i: ArrSize;

begin
    Get(i); -- здесь будет исключение Data_Error, если введёное значение не является числом от 1 до 10
    arr(i):=Pi;
    Put(arr(i));
endЕстественно, проверка рантаймная, а по другому никак, чудес не бывает...
Как вариант, процедура Get, инстанцированная для типа ArrSize, просто не позволит ввести значение, не являющееся числом от 1 до 10. Тогда никаких ошибок времени выполнения не будет...

[DIzer]

да из замкнутыми тоже... пример...
пусть у нас есть функция random( min, max) - генерирующая случайное целое число в диапазоне от min до max (вычисляющая член некоторой алгебраической последовательности)

Код: [Выделить]

var i:integer;
     a:array[1..10] of real;
begin
i:=random(5,15);
a[i]:=Pi; //аналогичный вопрос...
writeln(a[i])
end.


[DIzer]

Естественно, проверка рантаймная, а по другому никак, чудес не бывает...

И я про это..., а за одно про то что кое кому не стоит мозги ...ть простым людям.. ну по крайней  без необходимости..
 а вот шутки ради - пожалуйста   

[Geniepro]

пусть у нас есть функция random( min, max) - генерирующая случайное целое число в диапазоне от min до max (вычисляющая член некоторой алгебраической последовательности)

Код: [Выделить]

var i:integer;
     a:array[1..10] of real;
begin
i:=random(5,15);
a[i]:=Pi; //аналогичный вопрос...
writeln(a[i])
end.


У выражения random(5,15) тип, очевидно, Integer range 5 .. 15, что не совпадает с типом индекса массива Integer range 1 .. 10, так что будет просто ошибка компиляции -- несоответствие типов в выражении a(i):=Pi...

[DIzer]

пусть у нас есть функция random( min, max) - генерирующая случайное целое число в диапазоне от min до max (вычисляющая член некоторой алгебраической последовательности)

Код: [Выделить]

var i:integer;
     a:array[1..10] of real;
begin
i:=random(5,15);
a[i]:=Pi; //аналогичный вопрос...
writeln(a[i])
end.


У выражения random(5,15) тип, очевидно, Integer range 5 .. 15, что не совпадает с типом индекса массива Integer range 1 .. 10, так что будет просто ошибка компиляции -- несоответствие типов в выражении a(i):=Pi...

это знает ИСПОЛНИТЕЛЬ ЧЕЛОВЕК... а вот исполнитель "КОМПУТЕР" - НЕТ...

[DIzer]

хотя в данном случае вопрос решается переопределением функции random - она должна принимать аргументы вышеуказанного диапазона...- вопрос.. считать ли эту постановку эквивалентной начальной...