J.F wrote:

> Zastapienie moze nie byc takie latwe, jesli to jakis odporniejszy
> procesor, mozna gdzies wyczytac ze "formally verified", i jeszcze
> sprawdzony przez 25 lat ... chcesz cos nowoczesnego wstawic?

W US jest ciekawiej, bo certyfikat dostajesz an konkretne urządzenie
wykonane z konkretnych elementów. Potem się okazuje, że producent
opornika wycofał go z produkcji i zastąpił czymś innym -- i kosztowną
certyfikację zaczynasz od początku. Dlatego podstawą podstaw jest
wylistowanie w BOM kilku alternatywnych modeli przed rozpoczęciem
certyfikacji. Z zatwierdzonych alternatyw wolno Ci wybierać. :-)

Pozdrawiam, Piotr

do góry

On 30/04/2021 11:50, J.F wrote:
> OK, ale w Boeingu jest jakis lepszy procesor, to moze i C jest
> normalne.

Nie wiem. Wiem jednak, że jest tam za dużo procesorów kontrolujących
lot. Taka jest tendencja we wszystkim.

> A moze tez harwardzki, i kod z 51 sie przydaje :-)

Kod z '51 nigdzie się nie przydaje, poza Bytomiem i zegarem szkolnym.
Może jeszcze jakiś modemach GSM, ale tam napisano go w średniowieczu i
jest konsekrowany.

>> Jak by taka zależności RAM<->ogarnianie była prawdziwa...
> Latwiej zapanowac nad malym programem.

Nie wydaje mi się, 64kB to 64 tysiące mozliwości spieprzenia czegoś.
Weryfikacja formalna kodu nie będzie zastanawiać się ile masz pamięci
RAM, bardziej ile masz stanów osiągalnych bez synchronizacji itd.

>>> Ale czy zatrudniasz programistow w roznym wieku, czy starsi jakos tam
>>> dbaja o "ład korporacyjny" w pisaniu programow, uczą mlodszych jak to
>>> sie robi, czy zatrudniasz z doskoku i to najtanszych ...
>> Na końcu jest kontrola jakości. Jesli jest zrobiona na odpiernicz się
>> albo wcale, to programiści mają wypływ na jakość.
> Owszem, ale potem przychodzi deadline, kontrola mowi "tego nie mozemy
> wypuscic" a szef mowi "musimy" :-)

Takie rzeczy nie mogą miec miejsca, jeśli mówimy o poważnym sofcie od
którego zależy moje życie.

> Poza tym jak programista sie skupi na kontroli, to moze tak napisac
> program, ze testy przejdzie ...

I dostaniesz dobry program, jesli testy są dobre.

Jeśli testy są złe, wiele z nich można przejśc return 4;

Od testów zależy najwiecej.

>>> Hm. Make owszem, sie przydaje, ale wymaga narzedzi "command line".
>> Ciekawostka: przykładowo syntezer Xilinxa nie obsługuje command line.
>> Trzeba mu dostarczyć plik który interpretuje. Na dzień dobry wybija to
>> zęby pisząc makefile.
> IMO - i tak jest niezle, ze przewiduje taki plik,

W sensie że dziadostwo jest tylko o gram mniej dzadowskie ;) Widzę że
cieszysz się z małych rzeczy ;)

>> Bo make nie służy do robienia prototypów. Przypuszczalnie Photoshp też
>> nie ma wsparcia dla make.
> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
> setke zdjec z png na jpg" :-)

I tutaj wchodzi make, cały na biało, razem z kilkoma innymi toolami w
konsoli. Kończą, zanim Heniek odpali photoshopa i znajdzie w menu
funkcje konwersji. Ale Heniek będzie potem gadał wszystkim że on robi to
*prościej*, bo co łatwiejszego niż klikanie.

Innymi słowy prototyp sobie robisz w czymbądź. Produkcję ... nie,
produkcję potrafimy optymalizować narzędziami które pozoronie wydają się
być trudne w użyciu, jak syntezą z makefile, której nie da się zrobić,
bo Heńki. Błędne koło.

do góry

On Fri, 30 Apr 2021 12:21:16 +0200, Piotr Wyderski wrote:
> J.F wrote:
>> Zastapienie moze nie byc takie latwe, jesli to jakis odporniejszy
>> procesor, mozna gdzies wyczytac ze "formally verified", i jeszcze
>> sprawdzony przez 25 lat ... chcesz cos nowoczesnego wstawic?
>
> W US jest ciekawiej, bo certyfikat dostajesz an konkretne urządzenie
> wykonane z konkretnych elementów. Potem się okazuje, że producent
> opornika wycofał go z produkcji i zastąpił czymś innym -- i kosztowną
> certyfikację zaczynasz od początku. Dlatego podstawą podstaw jest
> wylistowanie w BOM kilku alternatywnych modeli przed rozpoczęciem
> certyfikacji. Z zatwierdzonych alternatyw wolno Ci wybierać. :-)

Hm, ale czy to nie powinno podnosic kosztow certyfikacji?

Czy jakos tak zakladamy, ze jesli opornik 100ohm/1W firmy X przeszedl
testy, to i opornik 100ohm/1W firmy Y tez przejdzie, skoro konstruktor
tak twierdzi.

Ewentualnie ... mozna by zmontowac kilka tych komputerow, z uzyciem
roznych elementow. Bez bawienia sie "kazdy z kazdym", ale tak zeby
kazdy zgloszony co najmniej w jednym urzadzeniu byl.
Dla opornikow moze bym i dopuscil taki tryb, ale czy bardziej
skomplikowane tez ?


J.

do góry

On Fri, 30 Apr 2021 12:45:55 +0200, heby wrote:
> On 30/04/2021 11:50, J.F wrote:
>> OK, ale w Boeingu jest jakis lepszy procesor, to moze i C jest
>> normalne.
> Nie wiem. Wiem jednak, że jest tam za dużo procesorów kontrolujących
> lot. Taka jest tendencja we wszystkim.
>
>> A moze tez harwardzki, i kod z 51 sie przydaje :-)
>
> Kod z '51 nigdzie się nie przydaje, poza Bytomiem i zegarem szkolnym.

W zasadzie tak, ale ... to skad to narzekanie na '51 ?

> Może jeszcze jakiś modemach GSM, ale tam napisano go w średniowieczu i
> jest konsekrowany.

Tam juz chyba cos lepszego potrzeba ... a moze nie?

>>> Jak by taka zależności RAM<->ogarnianie była prawdziwa...
>> Latwiej zapanowac nad malym programem.
>
> Nie wydaje mi się, 64kB to 64 tysiące mozliwości spieprzenia czegoś.
> Weryfikacja formalna kodu nie będzie zastanawiać się ile masz pamięci
> RAM, bardziej ile masz stanów osiągalnych bez synchronizacji itd.

Za to dosc istotne bedzie, jaki rozmiar ma ten kod zrodlowy.
W 64KB nie zmiescisz paru mln linii programu :-)

>>>> Ale czy zatrudniasz programistow w roznym wieku, czy starsi jakos tam
>>>> dbaja o "ład korporacyjny" w pisaniu programow, uczą mlodszych jak to
>>>> sie robi, czy zatrudniasz z doskoku i to najtanszych ...
>>> Na końcu jest kontrola jakości. Jesli jest zrobiona na odpiernicz się
>>> albo wcale, to programiści mają wypływ na jakość.
>> Owszem, ale potem przychodzi deadline, kontrola mowi "tego nie mozemy
>> wypuscic" a szef mowi "musimy" :-)
>
> Takie rzeczy nie mogą miec miejsca, jeśli mówimy o poważnym sofcie od
> którego zależy moje życie.

Dobrze piszesz ... ale szef ma nieco inny punkt widzenia :-)

>> Poza tym jak programista sie skupi na kontroli, to moze tak napisac
>> program, ze testy przejdzie ...
>
> I dostaniesz dobry program, jesli testy są dobre.

Musza byc bardzo szerokie.

> Jeśli testy są złe, wiele z nich można przejśc return 4;

OWszem, ale przewidzisz wszyskie sytuacje ?

>>>> Hm. Make owszem, sie przydaje, ale wymaga narzedzi "command line".
>>> Ciekawostka: przykładowo syntezer Xilinxa nie obsługuje command line.
>>> Trzeba mu dostarczyć plik który interpretuje. Na dzień dobry wybija to
>>> zęby pisząc makefile.
>> IMO - i tak jest niezle, ze przewiduje taki plik,
>
> W sensie że dziadostwo jest tylko o gram mniej dzadowskie ;) Widzę że
> cieszysz się z małych rzeczy ;)

Jakas tam automatyka moze juz z tego wyjsc.

>>> Bo make nie służy do robienia prototypów. Przypuszczalnie Photoshp też
>>> nie ma wsparcia dla make.
>> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
>> setke zdjec z png na jpg" :-)
>
> I tutaj wchodzi make, cały na biało, razem z kilkoma innymi toolami w
> konsoli.

O ile sa toole.

> Kończą, zanim Heniek odpali photoshopa i znajdzie w menu
> funkcje konwersji. Ale Heniek będzie potem gadał wszystkim że on robi to
> *prościej*, bo co łatwiejszego niż klikanie.

Bo tez moze byc odwrotnie - Heniek juz przerobil 100 plikow, co mu
zajelo 2 godziny, a oni ciagle czytaja dokumentacje :-)

J.

do góry

On 30/04/2021 13:22, J.F wrote:
>> Kod z '51 nigdzie się nie przydaje, poza Bytomiem i zegarem szkolnym.
> W zasadzie tak, ale ... to skad to narzekanie na '51 ?

Bo zostaly po nim techniki pisania kodu, które Heńki przenoszą na inne
dziedziny EDA.

>> Może jeszcze jakiś modemach GSM, ale tam napisano go w średniowieczu i
>> jest konsekrowany.
> Tam juz chyba cos lepszego potrzeba ... a moze nie?

Jakieś zastosowanie Bytomska najszybsza bryczka na świecie miała. Ponoć
w telefonach i ponoć w układach GSM. Masz wtedy 60x szybciej naliczanie
sekundowe i 200x dokładniejszy zegar uarta do komend AT!

>> Nie wydaje mi się, 64kB to 64 tysiące mozliwości spieprzenia czegoś.
>> Weryfikacja formalna kodu nie będzie zastanawiać się ile masz pamięci
>> RAM, bardziej ile masz stanów osiągalnych bez synchronizacji itd.
> Za to dosc istotne bedzie, jaki rozmiar ma ten kod zrodlowy.
> W 64KB nie zmiescisz paru mln linii programu :-)

Problem w tym, że to ma niewielkie znaczenie. Można mieć
nieweryfikowalny kod na tysiąc linijek i weryfikowalny na milion
zajmujacy gigabajt flash.

Kryterium pamieci czy długości kodu jest czynnikiem, ale raczej nie
decydującym, o możliwosciach stwierdzenia czy kod jest czy nie "dobry".

>>> Owszem, ale potem przychodzi deadline, kontrola mowi "tego nie mozemy
>>> wypuscic" a szef mowi "musimy" :-)
>> Takie rzeczy nie mogą miec miejsca, jeśli mówimy o poważnym sofcie od
>> którego zależy moje życie.
> Dobrze piszesz ... ale szef ma nieco inny punkt widzenia :-)

Dalej nie wydaje mi się aby crunching miał miejsce w firmie zajmującej
się produkcją poduszek powietrznych czy autopilotów. To nie kolejny
zegarek szkolny.

>>> Poza tym jak programista sie skupi na kontroli, to moze tak napisac
>>> program, ze testy przejdzie ...
>> I dostaniesz dobry program, jesli testy są dobre.
> Musza byc bardzo szerokie.

I są. Baza testów powinna być zdecydowanie większa niż kod, szczególnie
w zastosowaniach safety. Jaka będzie tego miara to inna sprawa, ale bez
wątpienia, ilość roboczogodzin napisanych na testy będzie większa niż na
kod.

>> Jeśli testy są złe, wiele z nich można przejśc return 4;
> OWszem, ale przewidzisz wszyskie sytuacje ?

Po to jest weryfikacja formalna aby przewidzieć *wszystkie*. Programista
ma tak pisać, aby mozna było *przynajmniej* wydzielić bloki kodu, które
są formalnie weryfikowalne lub są napisane w sposób pozwalajacy je
traktować i weryfikować osobno. To powoduje że testowanie wszystkiego
nie brzmi już tak utopijnie.

>>> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
>>> setke zdjec z png na jpg" :-)
>> I tutaj wchodzi make, cały na biało, razem z kilkoma innymi toolami w
>> konsoli.
> O ile sa toole.

Do tej konwersji? Na pęczki. Np. imagemagick.

>> Kończą, zanim Heniek odpali photoshopa i znajdzie w menu
>> funkcje konwersji. Ale Heniek będzie potem gadał wszystkim że on robi to
>> *prościej*, bo co łatwiejszego niż klikanie.
> Bo tez moze byc odwrotnie - Heniek juz przerobil 100 plikow, co mu
> zajelo 2 godziny, a oni ciagle czytaja dokumentacje :-)

I tu jest problem Heńka: 40 lat przeleciało za oknem i nagle trzeba się
orientować. Nic dziwnego że Heńkowie tak strasznie bronią swoich okopów
usypanych z 8051, TTLi i BC107 w których się orientują, przed śladem
złej innowacji.

do góry

On 30-Apr-21 11:17, heby wrote:
>
> I dlaczego LEON czy RISC-V miały być do tego gorszy niż Heńkowy 8051?

Formalnie nie są gorsze, są inne. Tak więc trzeba na nowo weryfikować
czy realtimowe założenia z Heńkowego 8051 są spełnione w nowej
architekturze.

> Nie przesadzajmy. Tych milionów lini kodu *NIKT* nie zweryfikował
> formalnie. Tam jest weryfikacja przez zasiedzenie. [...]

Tego nie wiemy ani (prawdopodobnie) Ty, ani ja ...
Jednakowoż po coś powymyślali DO-178 i inne wynalazki ...

> d... jeśli chodzi o weryfikację dużych systemów, niby rozwijamy się,
> tworzymy nowe metodyki, ale powiedz to Heńkowi, co gita na oczy nie
> widział.

A co Ty z tym git-em ciągle ... Jak Heniek ma certyfikowany proces
notowania w kajeciku która z nowych wersji jest najnowsza to ma się tego
trzymać a nie kombinować z git-em ...

> Zależy jacy programiści. Po tych w lotnictwie, spodziewam się że
> potrafią formalnie dowodzić przynajmniej kilkuset linijkowców dbających
> o bezpieczeństwo. Których pewnie nie ma, za to są wciśnięte właśnie
> kilkumilionowe potworki do sterowania autopilotem i sterowaniem klimą w
> jednym.

IMHO zupełnie niesłusznie się spodziewasz. Programiści nie są od
formalnego dowodzenia poprawności algorytmów ...

Piotrek

do góry

On Fri, 30 Apr 2021 13:48:43 +0200, heby wrote:
> On 30/04/2021 13:22, J.F wrote:
>>> Kod z '51 nigdzie się nie przydaje, poza Bytomiem i zegarem szkolnym.
>> W zasadzie tak, ale ... to skad to narzekanie na '51 ?
>
> Bo zostaly po nim techniki pisania kodu, które Heńki przenoszą na inne
> dziedziny EDA.

No nie wiem - to byl pewien margines, a kod zazwyczaj w assemblerze
:-)

>>> Może jeszcze jakiś modemach GSM, ale tam napisano go w średniowieczu i
>>> jest konsekrowany.
>> Tam juz chyba cos lepszego potrzeba ... a moze nie?
>
> Jakieś zastosowanie Bytomska najszybsza bryczka na świecie miała. Ponoć
> w telefonach i ponoć w układach GSM. Masz wtedy 60x szybciej naliczanie
> sekundowe i 200x dokładniejszy zegar uarta do komend AT!

ale czy obsluga GSM nie wymaga czegos lepszego?
No chyba ze - do GSM byl osobny uklad/y, a 51 robil tylko gdzies w
interfejsie.

>>> Nie wydaje mi się, 64kB to 64 tysiące mozliwości spieprzenia czegoś.
>>> Weryfikacja formalna kodu nie będzie zastanawiać się ile masz pamięci
>>> RAM, bardziej ile masz stanów osiągalnych bez synchronizacji itd.
>> Za to dosc istotne bedzie, jaki rozmiar ma ten kod zrodlowy.
>> W 64KB nie zmiescisz paru mln linii programu :-)
>
> Problem w tym, że to ma niewielkie znaczenie. Można mieć
> nieweryfikowalny kod na tysiąc linijek i weryfikowalny na milion
> zajmujacy gigabajt flash.
>
> Kryterium pamieci czy długości kodu jest czynnikiem, ale raczej nie
> decydującym, o możliwosciach stwierdzenia czy kod jest czy nie "dobry".

Ale zweryfikowac kod o milionie linii jest zdecydowanie trudniej i
drozej :-)

>>>> Owszem, ale potem przychodzi deadline, kontrola mowi "tego nie mozemy
>>>> wypuscic" a szef mowi "musimy" :-)
>>> Takie rzeczy nie mogą miec miejsca, jeśli mówimy o poważnym sofcie od
>>> którego zależy moje życie.
>> Dobrze piszesz ... ale szef ma nieco inny punkt widzenia :-)
>
> Dalej nie wydaje mi się aby crunching miał miejsce w firmie zajmującej
> się produkcją poduszek powietrznych czy autopilotów. To nie kolejny
> zegarek szkolny.

no, 737MAX troche Boeingowi nie wyszedl.

>>>> Poza tym jak programista sie skupi na kontroli, to moze tak napisac
>>>> program, ze testy przejdzie ...
>>> I dostaniesz dobry program, jesli testy są dobre.
>> Musza byc bardzo szerokie.
>
> I są. Baza testów powinna być zdecydowanie większa niż kod, szczególnie
> w zastosowaniach safety. Jaka będzie tego miara to inna sprawa, ale bez
> wątpienia, ilość roboczogodzin napisanych na testy będzie większa niż na
> kod.

>>> Jeśli testy są złe, wiele z nich można przejśc return 4;
>> OWszem, ale przewidzisz wszyskie sytuacje ?
>
> Po to jest weryfikacja formalna aby przewidzieć *wszystkie*.

Ale to jest obok testow. Jak myslisz, ze testy nalepsze i wszystko
wylapia ...
Z drugiej strony - jak sie mozna pomylic przy algorytmie, przy pisaniu
programu - tak mozna i przy weryfikacji.
A test na symulatorze ... moze wylapie blad.

>>>> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
>>>> setke zdjec z png na jpg" :-)
>>> I tutaj wchodzi make, cały na biało, razem z kilkoma innymi toolami w
>>> konsoli.
>> O ile sa toole.
>
> Do tej konwersji? Na pęczki. Np. imagemagick.

Ale jak to wszystko w windows - najlepiej obsluguje sie myszka :-)

>>> Kończą, zanim Heniek odpali photoshopa i znajdzie w menu
>>> funkcje konwersji. Ale Heniek będzie potem gadał wszystkim że on robi to
>>> *prościej*, bo co łatwiejszego niż klikanie.
>> Bo tez moze byc odwrotnie - Heniek juz przerobil 100 plikow, co mu
>> zajelo 2 godziny, a oni ciagle czytaja dokumentacje :-)
>
> I tu jest problem Heńka: 40 lat przeleciało za oknem i nagle trzeba się
> orientować. Nic dziwnego że Heńkowie tak strasznie bronią swoich okopów

W tym przykladzie to IMO niekoniecznie - Heniek z niechecia przerobil
te 100 plikow ... ale tak bylo najprosciej.

> usypanych z 8051, TTLi i BC107 w których się orientują, przed śladem
> złej innowacji.

J.

do góry

On Fri, 30 Apr 2021 11:50:26 +0200, "J.F"
<j...@p...onet.pl> wrote:
> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
> setke zdjec z png na jpg" :-)

Przecież to ogarnia 6 letnie dziecko w bash'u:

$ for i in *.jpg; do f=`basename $i .png`; convert $f.jpg $f.png;
done

--
Marek

do góry

On Fri, 30 Apr 2021 14:27:36 +0200, Marek <f...@f...com> wrote:
> $ for i in *.jpg; do f=`basename $i .png`; convert $f.jpg $f.png;
> done

basename $i .jpg oczywiście.

--
Marek

do góry

On Fri, 30 Apr 2021 14:27:36 +0200, Marek wrote:
> On Fri, 30 Apr 2021 11:50:26 +0200, "J.F"
> <j...@p...onet.pl> wrote:
>> A potem masz zadanie "redakcja nie chce png tylko jpg. Jak przerobic
>> setke zdjec z png na jpg" :-)
>
> Przecież to ogarnia 6 letnie dziecko w bash'u:
>
> $ for i in *.jpg; do f=`basename $i .png`; convert $f.jpg $f.png;
> done

Ogarnia, jesli masz taki zgrabny program convert.
A zaplaciles za Photoshopa i jego chcesz wykorzystac.

Zreszta *** wie jak ten convert sobie radzi z zapisaniem do jpg.
Tam jest pare parametrow.
A PS dobrze sobie radzi, przynajmniej prawie wszyscy zawodowcy tak
uwazaja :-P

J.

do góry